defpred S₁[ set , set ] means $2 = (G . $1) * (F . $1);
A1: for i being set st i in (dom F) /\ (dom G) holds
ex u being set st S₁[i,u] ;
consider H being Function such that
A2: ( dom H = (dom F) /\ (dom G) & ( for i being set st i in (dom F) /\ (dom G) holds
S₁[i,H . i] ) ) from CLASSES1:sch 1(A1);
for x being set st x in dom H holds
H . x is Function

proof

let x be set ; :: thesis: ( x in dom H implies H . x is Function )
reconsider f = F . x as Function ;
reconsider g = G . x as Function ;
assume x in dom H ; :: thesis: H . x is Function
then H . x = g * f by A2;
hence H . x is Function ; :: thesis: verum

end;

then reconsider H = H as Function-yielding Function by FUNCOP_1:def 6;
take H ; :: thesis: ( dom H = (dom F) /\ (dom G) & ( for i being set st i in dom H holds
H . i = (G . i) * (F . i) ) )
thus ( dom H = (dom F) /\ (dom G) & ( for i being set st i in dom H holds
H . i = (G . i) * (F . i) ) ) by A2; :: thesis: verum