defpred S₁[ set , set ] means ex o being object of A st
( $1 = o & $2 = idm (F . o) );
A1: for a being Element of A ex j being set st S₁[a,j]

proof

let a be Element of A; :: thesis: ex j being set st S₁[a,j]
reconsider o = a as object of A ;
ex j being set st j = idm (F . o) ;
hence ex j being set st S₁[a,j] ; :: thesis: verum

end;

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 o be Element of A; :: thesis: t . o is Morphism of (F . o),(F . o)
ex a being object of A st
( o = a & t . o = idm (F . a) ) by A2;
hence t . o is Morphism of (F . o),(F . o) ; :: thesis: verum

end;

then reconsider t = t as transformation of F,F by Def2;
take t ; :: thesis: for a being object of A holds t . a = idm (F . a)
let a be Element of A; :: thesis: t . a = idm (F . a)
ex o being object of A st
( a = o & t . a = idm (F . o) ) by A2;
hence t . a = idm (F . a) ; :: thesis: verum