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 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 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 A6: for r being 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 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 A7: for r being 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 :: thesis: for r being Element of REAL
for x being Element of [: the carrier of G, the carrier of F:] holds H1 . (r,x) = H2 . (r,x)

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
A8: x = [x1,x2] by Lm1;
thus H1 . (r,x) = [(r * x1),(r * x2)] by A6, A8
.= H2 . (r,x) by A7, A8 ; :: thesis: verum

end;

hence H1 = H2 ; :: thesis: verum