now

let x be Point of [:G,F:]; :: thesis: ( x = 0. [:G,F:] implies ||.x.|| = 0 )
consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
consider v being Element of REAL 2 such that
A11: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by defNORM;
assume x = 0. [:G,F:] ; :: thesis: ||.x.|| = 0
then ( x1 = 0. G & x2 = 0. F ) by P1, ZFMISC_1:33;
then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) ;
then v = 0* 2 by A11, FINSEQ_2:75;
hence ||.x.|| = 0 by A11, P1, EUCLID:10; :: thesis: verum

end;

then ||.(0. [:G,F:]).|| = 0 ;
hence [:G,F:] is reflexive by NORMSP_0:def 6; :: thesis: ( [:G,F:] is discerning & [:G,F:] is RealNormSpace-like )

now

let x be Point of [:G,F:]; :: thesis: ( ||.x.|| = 0 implies x = 0. [:G,F:] )
consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
consider v being Element of REAL 2 such that
A11: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by defNORM;
assume ||.x.|| = 0 ; :: thesis: x = 0. [:G,F:]
then v = 0* 2 by A11, P1, EUCLID:11;
then X0: v = <*0,0*> by FINSEQ_2:75;
( ||.x1.|| = v . 1 & ||.x2.|| = v . 2 ) by A11, FINSEQ_1:61;
then ( ||.x1.|| = 0 & ||.x2.|| = 0 ) by X0, FINSEQ_1:61;
then ( x1 = 0. G & x2 = 0. F ) by NORMSP_0:def 5;
hence x = 0. [:G,F:] by P1; :: thesis: verum

end;

hence [:G,F:] is discerning by NORMSP_0:def 5; :: thesis: [:G,F:] is RealNormSpace-like

now

let x, y be Point of [:G,F:]; :: thesis: for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; :: thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
consider y1 being Point of G, y2 being Point of F such that
P2: y = [y1,y2] by LM01;
consider v being Element of REAL 2 such that
A11: ( v = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.v.| ) by defNORM;
consider z being Element of REAL 2 such that
A21: ( z = <*||.y1.||,||.y2.||*> & (prod_NORM (G,F)) . (y1,y2) = |.z.| ) by defNORM;
thus ||.(a * x).|| = (abs a) * ||.x.|| :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

proof

consider w being Element of REAL 2 such that
X1: ( w = <*||.(a * x1).||,||.(a * x2).||*> & (prod_NORM (G,F)) . ((a * x1),(a * x2)) = |.w.| ) by defNORM;
reconsider aa = abs a, xx1 = ||.x1.||, xx2 = ||.x2.|| as real number ;
( ||.(a * x1).|| = (abs a) * ||.x1.|| & ||.(a * x2).|| = (abs a) * ||.x2.|| ) by NORMSP_1:def 2;
then w = aa * |[xx1,xx2]| by X1, EUCLID:62
.= (abs a) * v by A11, EUCLID:69 ;
then |.w.| = (abs (abs a)) * |.v.| by EUCLID:14
.= (abs a) * |.v.| ;
hence ||.(a * x).|| = (abs a) * ||.x.|| by A11, X1, P1, defMLT; :: thesis: verum

end;

thus ||.(x + y).|| <= ||.x.|| + ||.y.|| :: thesis: verum

proof

consider w being Element of REAL 2 such that
X1: ( w = <*||.(x1 + y1).||,||.(x2 + y2).||*> & (prod_NORM (G,F)) . ((x1 + y1),(x2 + y2)) = |.w.| ) by defNORM;
X4: ||.(x + y).|| = |.w.| by X1, P1, P2, defADD;
X5: ( ||.(x1 + y1).|| <= ||.x1.|| + ||.y1.|| & ||.(x2 + y2).|| <= ||.x2.|| + ||.y2.|| ) by NORMSP_1:def 2;
set t = <*(||.x1.|| + ||.y1.||),(||.x2.|| + ||.y2.||)*>;
reconsider t = <*(||.x1.|| + ||.y1.||),(||.x2.|| + ||.y2.||)*> as FinSequence of REAL ;
X6: ( len w = 2 & len t = 2 ) by FINSEQ_1:61, X1;

now

let i be Element of NAT ; :: thesis: ( i in Seg (len w) implies ( 0 <= w . b₁ & w . b₁ <= t . b₁ ) )
assume i in Seg (len w) ; :: thesis: ( 0 <= w . b₁ & w . b₁ <= t . b₁ )
then X62: i in Seg 2 by FINSEQ_1:61, X1;

per cases ( i = 1 or i = 2 ) by X62, FINSEQ_1:4, TARSKI:def 2;

suppose X63: i = 1 ; :: thesis: ( 0 <= w . b₁ & w . b₁ <= t . b₁ )

then w . i = ||.(x1 + y1).|| by X1, FINSEQ_1:61;
hence ( 0 <= w . i & w . i <= t . i ) by X5, X63, FINSEQ_1:61, NORMSP_1:8; :: thesis: verum

end;

suppose X64: i = 2 ; :: thesis: ( 0 <= w . b₁ & w . b₁ <= t . b₁ )

then w . i = ||.(x2 + y2).|| by X1, FINSEQ_1:61;
hence ( 0 <= w . i & w . i <= t . i ) by X5, X64, FINSEQ_1:61, NORMSP_1:8; :: thesis: verum

end;

end;

end;

then X7: |.w.| <= |.t.| by PRVECT_2:2, X6;
t = |[||.x1.||,||.x2.||]| + |[||.y1.||,||.y2.||]| by EUCLID:60
.= v + z by A11, A21, EUCLID:68 ;
then |.t.| <= |.v.| + |.z.| by EUCLID:15;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by X4, P1, A11, P2, A21, XXREAL_0:2, X7; :: thesis: verum

end;

end;

hence [:G,F:] is RealNormSpace-like by NORMSP_1:def 2; :: thesis: verum