let H1, H2 be Function of [: the carrier of G, the carrier of F:],REAL; ( ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H1 . (g,f) = |.v.| ) ) & ( for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H2 . (g,f) = |.v.| ) ) implies H1 = H2 )
assume A4:
for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H1 . (g,f) = |.v.| )
; ( ex g being Point of G ex f being Point of F st
for v being Element of REAL 2 holds
( not v = <*||.g.||,||.f.||*> or not H2 . (g,f) = |.v.| ) or H1 = H2 )
assume A5:
for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & H2 . (g,f) = |.v.| )
; H1 = H2
now for g being Element of the carrier of G
for f being Element of the carrier of F holds H1 . (g,f) = H2 . (g,f)let g be
Element of the
carrier of
G;
for f being Element of the carrier of F holds H1 . (g,f) = H2 . (g,f)let f be
Element of the
carrier of
F;
H1 . (g,f) = H2 . (g,f)A6:
ex
v1 being
Element of
REAL 2 st
(
v1 = <*||.g.||,||.f.||*> &
H1 . (
g,
f)
= |.v1.| )
by A4;
ex
v2 being
Element of
REAL 2 st
(
v2 = <*||.g.||,||.f.||*> &
H2 . (
g,
f)
= |.v2.| )
by A5;
hence
H1 . (
g,
f)
= H2 . (
g,
f)
by A6;
verum end;
hence
H1 = H2
; verum