theorem Th14:
for
E,
F,
G being
RealNormSpace holds
( ( for
x being
set holds
(
x is
Point of
[:E,F,G:] iff ex
x1 being
Point of
E ex
x2 being
Point of
F ex
x3 being
Point of
G st
x = [x1,x2,x3] ) ) & ( for
x1,
y1 being
Point of
E for
x2,
y2 being
Point of
F for
x3,
y3 being
Point of
G holds
[x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] ) &
0. [:E,F,G:] = [(0. E),(0. F),(0. G)] & ( for
x1 being
Point of
E for
x2 being
Point of
F for
x3 being
Point of
G for
a being
Real holds
a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)] ) & ( for
x1 being
Point of
E for
x2 being
Point of
F for
x3 being
Point of
G holds
- [x1,x2,x3] = [(- x1),(- x2),(- x3)] ) & ( for
x1 being
Point of
E for
x2 being
Point of
F for
x3 being
Point of
G holds
(
||.[x1,x2,x3].|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex
w being
Element of
REAL 3 st
(
w = <*||.x1.||,||.x2.||,||.x3.||*> &
||.[x1,x2,x3].|| = |.w.| ) ) ) )