package Protected_Func with SPARK_Mode is
   protected Prot_Obj is
      function Prot_Func return Integer;
   private
      Comp : Integer := 0;
   end Prot_Obj;

   Part_Of_Constit : Integer := 0 with Part_Of => Prot_Obj;
end Protected_Func;