theorem :: PRVECT_3:19

for G, F being RealNormSpace holds
( ( for x being set holds
( x is Point of (product <*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 (product <*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. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Point of (product <*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 (product <*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 (product <*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.| ) ) )