defpred S_{1}[ Object of A, object ] means $2 = idm (F . $1);

A1: for a being Element of A ex j being object st S_{1}[a,j]
;

consider t being ManySortedSet of the carrier of A such that

A2: for a being Element of A holds S_{1}[a,t . a]
from PBOOLE:sch 6(A1);

for a being Object of A holds t . a is Morphism of (F . a),(F . a)

hence ex b_{1} being transformation of F,F st

for a being Object of A holds b_{1} . a = idm (F . a)
by A2; :: thesis: verum

A1: for a being Element of A ex j being object st S

consider t being ManySortedSet of the carrier of A such that

A2: for a being Element of A holds S

for a being Object of A holds t . a is Morphism of (F . a),(F . a)

proof

then
t is transformation of F,F
by Def2;
let a be Element of A; :: thesis: t . a is Morphism of (F . a),(F . a)

S_{1}[a,t . a]
by A2;

hence t . a is Morphism of (F . a),(F . a) ; :: thesis: verum

end;S

hence t . a is Morphism of (F . a),(F . a) ; :: thesis: verum

hence ex b

for a being Object of A holds b