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:]; ( ( 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)]
; ( 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)]
; H1 = H2
now 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;
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:];
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
;
verum end;
hence
H1 = H2
; verum