let H1, H2 be Function; :: thesis: ( dom H1 = (dom F) /\ (dom G) & ( for i being set st i in dom H1 holds
H1 . i = (G . i) * (F . i) ) & dom H2 = (dom F) /\ (dom G) & ( for i being set st i in dom H2 holds
H2 . i = (G . i) * (F . i) ) implies H1 = H2 )
assume that
A3: dom H1 = (dom F) /\ (dom G) and
A4: for i being set st i in dom H1 holds
H1 . i = (G . i) * (F . i) and
A5: dom H2 = (dom F) /\ (dom G) and
A6: for i being set st i in dom H2 holds
H2 . i = (G . i) * (F . i) ; :: thesis: H1 = H2

now

let i be set ; :: thesis: ( i in (dom F) /\ (dom G) implies H1 . i = H2 . i )
reconsider f = F . i as Function ;
reconsider g = G . i as Function ;
assume A7: i in (dom F) /\ (dom G) ; :: thesis: H1 . i = H2 . i
then H1 . i = g * f by A3, A4;
hence H1 . i = H2 . i by A5, A6, A7; :: thesis: verum

end;

hence H1 = H2 by A3, A5, FUNCT_1:2; :: thesis: verum