set I = (dom F) /\ (dom f);

defpred S_{1}[ 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_{1}[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_{1}[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

defpred S

A1: for i being object st i in (dom F) /\ (dom f) holds

ex y being object st S

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

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