let G, F be non empty NORMSTR ; :: thesis: ex NORMGF being Function of [: the carrier of G, the carrier of F:],REAL st
for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| )
defpred S₁[ set , set , set ] means ex g being Point of G ex f being Point of F ex v being Element of REAL 2 st
( $1 = g & $2 = f & v = <*||.g.||,||.f.||*> & $3 = |.v.| );
P1: for x, y being set st x in the carrier of G & y in the carrier of F holds
ex z being set st
( z in REAL & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in the carrier of G & y in the carrier of F implies ex z being set st
( z in REAL & S₁[x,y,z] ) )
assume AS1: ( x in the carrier of G & y in the carrier of F ) ; :: thesis: ex z being set st
( z in REAL & S₁[x,y,z] )
then reconsider g = x as Point of G ;
reconsider f = y as Point of F by AS1;
reconsider v = <*||.g.||,||.f.||*> as Element of REAL 2 by FINSEQ_2:121;
|.v.| in REAL ;
hence ex z being set st
( z in REAL & S₁[x,y,z] ) ; :: thesis: verum

end;

consider NORMGF being Function of [: the carrier of G, the carrier of F:],REAL such that
P2: for x, y being set st x in the carrier of G & y in the carrier of F holds
S₁[x,y,NORMGF . (x,y)] from BINOP_1:sch 1(P1);

now

let g be Point of G; :: thesis: for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| )
let f be Point of F; :: thesis: ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| )
ex gg being Point of G ex ff being Point of F ex v being Element of REAL 2 st
( g = gg & f = ff & v = <*||.gg.||,||.ff.||*> & NORMGF . (g,f) = |.v.| ) by P2;
hence ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) ; :: thesis: verum

end;

hence ex NORMGF being Function of [: the carrier of G, the carrier of F:],REAL st
for g being Point of G
for f being Point of F ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) ; :: thesis: verum