let H1, H2 be Function-yielding 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
A4: ( dom H1 = (dom F) /\ (dom G) & ( for i being set st i in dom H1 holds
H1 . i = (G . i) * (F . i) ) ) and
A5: ( dom H2 = (dom F) /\ (dom G) & ( 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 )
assume A6: i in (dom F) /\ (dom G) ; :: thesis: H1 . i = H2 . i
reconsider f = F . i as Function ;
reconsider g = G . i as Function ;
( H1 . i = g * f & H2 . i = g * f ) by A4, A5, A6;
hence H1 . i = H2 . i ; :: thesis: verum

end;

hence H1 = H2 by A4, A5, FUNCT_1:9; :: thesis: verum