defpred S₁[ object , object ] means $2 = (G . $1) * (F . $1);
A1: for i being object st i in (dom F) /\ (dom G) holds
ex u being object st S₁[i,u] ;
ex H being Function st
( dom H = (dom F) /\ (dom G) & ( for i being object st i in (dom F) /\ (dom G) holds
S₁[i,H . i] ) ) from CLASSES1:sch 1(A1);
hence ex b₁ being Function st
( dom b₁ = (dom F) /\ (dom G) & ( for i being object st i in dom b₁ holds
b₁ . i = (G . i) * (F . i) ) ) ; :: thesis: verum