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

now :: thesis: for r being Element of the carrier of K
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 the carrier of K; :: 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)
[: the carrier of G, the carrier of F:] <> {} by ZFMISC_1:90;
then consider x1 being Element of G, x2 being Element of F such that
A8: x = [x1,x2] by SUBSET_1:43;
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