theorem Th12: :: LOPBAN14:11

for G being RealNormSpace holds
( ( for x being set holds
( x is Point of (product <*G*>) iff ex x1 being Point of G st x = <*x1*> ) ) & ( for x, y being Point of (product <*G*>)
for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*> ) & 0. (product <*G*>) = <*(0. G)*> & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
||.x.|| = ||.x1.|| ) )