theorem Th18:
for
G,
F being
RealNormSpace holds
( ( 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.| ) ) )