defpred S₁[ Object of A, object ] means $2 = idm (F . $1);
A1: for a being Element of A ex j being object st S₁[a,j] ;
consider t being ManySortedSet of the carrier of A such that
A2: for a being Element of A holds S₁[a,t . a] from PBOOLE:sch 6(A1);
for a being Object of A holds t . a is Morphism of (F . a),(F . a)

proof

let a be Element of A; :: thesis: t . a is Morphism of (F . a),(F . a)
S₁[a,t . a] by A2;
hence t . a is Morphism of (F . a),(F . a) ; :: thesis: verum

end;

then t is transformation of F,F by Def2;
hence ex b₁ being transformation of F,F st
for a being Object of A holds b₁ . a = idm (F . a) by A2; :: thesis: verum