set I = dom F;
defpred S₁[ set , set ] means $2 = (F . $1) . (f . $1);
A1: for i being set st i in dom F holds
ex y being set st S₁[i,y] ;
consider F being Function such that
A2: ( dom F = dom F & ( for i being set st i in dom F holds
S₁[i,F . i] ) ) from CLASSES1:sch 1(A1);
take F ; :: thesis: ( dom F = dom F & ( for x being set st x in dom F holds
F . x = (F . x) . (f . x) ) )
thus ( dom F = dom F & ( for x being set st x in dom F holds
F . x = (F . x) . (f . x) ) ) by A2; :: thesis: verum