let H1, H2 be Function of [:REAL,[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:]; :: thesis: ( ( for r being Element of REAL
for g being Point of G
for f being Point of F holds H1 . (r,[g,f]) = [(r * g),(r * f)] ) & ( for r being Element of REAL
for g being Point of G
for f being Point of F holds H2 . (r,[g,f]) = [(r * g),(r * f)] ) implies H1 = H2 )
assume A1: for r being Element of REAL
for g being Point of G
for f being Point of F holds H1 . (r,[g,f]) = [(r * g),(r * f)] ; :: thesis: ( ex r being Element of REAL ex g being Point of G ex f being Point of F st not H2 . (r,[g,f]) = [(r * g),(r * f)] or H1 = H2 )
assume A2: for r being Element of REAL
for g being Point of G
for f being Point of F holds H2 . (r,[g,f]) = [(r * g),(r * f)] ; :: thesis: H1 = H2

now

let r be Element of REAL ; :: thesis: for x being Element of [: the carrier of G, the carrier of F:] holds H1 . (r,x) = H2 . (r,x)
let x be Element of [: the carrier of G, the carrier of F:]; :: thesis: H1 . (r,x) = H2 . (r,x)
consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
thus H1 . (r,x) = [(r * x1),(r * x2)] by A1, P1
.= H2 . (r,x) by A2, P1 ; :: thesis: verum

end;

hence H1 = H2 by BINOP_1:2; :: thesis: verum