deffunc H₁( object ) -> set = proj (A,$1);
consider P being ManySortedSet of I such that
A2: for i being object st i in I holds
P . i = H₁(i) from PBOOLE:sch 4();
set B = EnsCatProductObj A;
A3: EnsCatProductObj A = product A by A1, Def10;
P is MorphismsFamily of EnsCatProductObj A,A

proof

let i be object ; :: according to ALTCAT_5:def 2 :: thesis: ( i in I implies ex o1 being Object of (EnsCat E) st
( o1 = A . i & P . i is Morphism of (EnsCatProductObj A),o1 ) )
assume A4: i in I ; :: thesis: ex o1 being Object of (EnsCat E) st
( o1 = A . i & P . i is Morphism of (EnsCatProductObj A),o1 )
reconsider I = I as non empty set by A4;
reconsider i = i as Element of I by A4;
reconsider A = A as ObjectsFamily of I,(EnsCat E) ;
take A . i ; :: thesis: ( A . i = A . i & P . i is Morphism of (EnsCatProductObj A),(A . i) )
A5: <^(EnsCatProductObj A),(A . i)^> = Funcs ((EnsCatProductObj A),(A . i)) by ALTCAT_1:def 14;
dom A = I by PARTFUN1:def 2;
then A6: rng (proj (A,i)) c= A . i by YELLOW17:3;
dom (proj (A,i)) = EnsCatProductObj A by A3, PARTFUN1:def 2;
then proj (A,i) in Funcs ((EnsCatProductObj A),(A . i)) by A6, FUNCT_2:def 2;
hence ( A . i = A . i & P . i is Morphism of (EnsCatProductObj A),(A . i) ) by A2, A5; :: thesis: verum

end;

then reconsider P = P as MorphismsFamily of EnsCatProductObj A,A ;
take P ; :: thesis: for i being set st i in I holds
P . i = proj (A,i)
thus for i being set st i in I holds
P . i = proj (A,i) by A2; :: thesis: verum