defpred S₁[ object , object , object ] 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.| );
A1: for x, y being object st x in the carrier of G & y in the carrier of F holds
ex z being object st
( z in REAL & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in the carrier of G & y in the carrier of F implies ex z being object st
( z in REAL & S₁[x,y,z] ) )
assume A2: ( x in the carrier of G & y in the carrier of F ) ; :: thesis: ex z being object st
( z in REAL & S₁[x,y,z] )
then reconsider g = x as Point of G ;
reconsider f = y as Point of F by A2;
reconsider v = <*||.g.||,||.f.||*> as Element of REAL 2 by FINSEQ_2:101;
|.v.| in REAL by XREAL_0:def 1;
hence ex z being object 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
A3: for x, y being object 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(A1);

now :: thesis: 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.| )

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 A3;
hence ex v being Element of REAL 2 st
( v = <*||.g.||,||.f.||*> & NORMGF . (g,f) = |.v.| ) ; :: thesis: verum

end;

hence ex b₁ 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.||*> & b₁ . (g,f) = |.v.| ) ; :: thesis: verum