let H1, H2 be Function of [: the carrier of G, the carrier of F:],REAL; :: thesis: ( ( 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.| ) ; :: thesis: ( 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.| ) ; :: thesis: H1 = H2

now :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence H1 = H2 ; :: thesis: verum