let G, F be RealNormSpace; :: thesis: ( ( for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) ) & ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )
thus for x being set holds
( x is Point of [:G,F:] iff ex x1 being Point of G ex x2 being Point of F st x = [x1,x2] ) by Lm1; :: thesis: ( ( for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) & 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )
thus for x, y being Point of [:G,F:]
for x1, y1 being Point of G
for x2, y2 being Point of F st x = [x1,x2] & y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] by Def1; :: thesis: ( 0. [:G,F:] = [(0. G),(0. F)] & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )
thus 0. [:G,F:] = [(0. G),(0. F)] ; :: thesis: ( ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )
thus for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)] :: thesis: ( ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] ) & ( for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) ) )

proof

let x be Point of [:G,F:]; :: thesis: for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x1 be Point of G; :: thesis: for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x2 be Point of F; :: thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )
assume A1: x = [x1,x2] ; :: thesis: - x = [(- x1),(- x2)]
reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ;
x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1
.= [(0. G),(x2 + (- x2))] by RLVECT_1:def 10
.= 0. [:G,F:] by RLVECT_1:def 10 ;
hence - x = [(- x1),(- x2)] by RLVECT_1:def 10; :: thesis: verum

end;

thus for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F
for a being Real st x = [x1,x2] holds
a * x = [(a * x1),(a * x2)] by Def2; :: thesis: for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
thus for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) :: thesis: verum

proof

let x be Point of [:G,F:]; :: thesis: for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
let x1 be Point of G; :: thesis: for x2 being Point of F st x = [x1,x2] holds
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
let x2 be Point of F; :: thesis: ( x = [x1,x2] implies ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) )
assume A2: x = [x1,x2] ; :: thesis: ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| )
ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & (prod_NORM (G,F)) . (x1,x2) = |.w.| ) by Def6;
hence ex w being Element of REAL 2 st
( w = <*||.x1.||,||.x2.||*> & ||.x.|| = |.w.| ) by A2; :: thesis: verum

end;