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

now :: thesis: for i being object st i in (dom F) /\ (dom G) holds
H1 . i = H2 . i

let i be object ; :: 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 A6: i in (dom F) /\ (dom G) ; :: thesis: H1 . i = H2 . i
then H1 . i = g * f by A2, A3;
hence H1 . i = H2 . i by A4, A5, A6; :: thesis: verum

end;

hence H1 = H2 by A2, A4; :: thesis: verum