set I = dom F;
defpred S₁[ object , object ] means $2 = (F . $1) . (f . $1);
A1: for i being object st i in dom F holds
ex y being object st S₁[i,y] ;
consider F being Function such that
A2: ( dom F = dom F & ( for i being object 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