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