let E, F, G be RealNormSpace; :: thesis: ( ( 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.| ) ) ) )
thus 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] ) :: thesis: ( ( 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.| ) ) ) )

proof

let x be set ; :: thesis: ( 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] )

hereby :: thesis: ( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] implies x is Point of [:E,F,G:] )

assume x is Point of [:E,F,G:] ; :: thesis: ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
then consider x1x2 being Point of [:E,F:], x3 being Point of G such that
A1: x = [x1x2,x3] by PRVECT_3:18;
consider x1 being Point of E, x2 being Point of F such that
A2: x1x2 = [x1,x2] by PRVECT_3:18;
take x1 = x1; :: thesis: ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
take x2 = x2; :: thesis: ex x3 being Point of G st x = [x1,x2,x3]
take x3 = x3; :: thesis: x = [x1,x2,x3]
thus x = [x1,x2,x3] by A1, A2; :: thesis: verum

end;

thus ( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] implies x is Point of [:E,F,G:] ) ; :: thesis: verum

end;

hereby :: thesis: ( 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.| ) ) ) )

let x1, y1 be Point of E; :: thesis: 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)]
let x2, y2 be Point of F; :: thesis: for x3, y3 being Point of G holds [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)]
let x3, y3 be Point of G; :: thesis: [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)]
[x1,x2] + [y1,y2] = [(x1 + y1),(x2 + y2)] by PRVECT_3:18;
hence [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by PRVECT_3:18; :: thesis: verum

end;

thus 0. [:E,F,G:] = [(0. E),(0. F),(0. G)] ; :: thesis: ( ( 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.| ) ) ) )
thus A7: 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)] :: thesis: ( ( 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.| ) ) ) )

proof

let x1 be Point of E; :: thesis: 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)]
let x2 be Point of F; :: thesis: for x3 being Point of G
for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]
let x3 be Point of G; :: thesis: for a being Real holds a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]
let a be Real; :: thesis: a * [x1,x2,x3] = [(a * x1),(a * x2),(a * x3)]
thus a * [x1,x2,x3] = [(a * [x1,x2]),(a * x3)] by PRVECT_3:18
.= [(a * x1),(a * x2),(a * x3)] by PRVECT_3:18 ; :: thesis: verum

end;

hereby :: thesis: 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.| ) )

let x1 be Point of E; :: thesis: for x2 being Point of F
for x3 being Point of G holds - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
let x2 be Point of F; :: thesis: for x3 being Point of G holds - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
let x3 be Point of G; :: thesis: - [x1,x2,x3] = [(- x1),(- x2),(- x3)]
thus - [x1,x2,x3] = (- 1) * [x1,x2,x3] by RLVECT_1:16
.= [((- 1) * x1),((- 1) * x2),((- 1) * x3)] by A7
.= [(- x1),((- 1) * x2),((- 1) * x3)] by RLVECT_1:16
.= [(- x1),(- x2),((- 1) * x3)] by RLVECT_1:16
.= [(- x1),(- x2),(- x3)] by RLVECT_1:16 ; :: thesis: verum

end;

let x1 be Point of E; :: thesis: 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.| ) )
let y1 be Point of F; :: thesis: for x3 being Point of G holds
( ||.[x1,y1,x3].|| = sqrt (((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st
( w = <*||.x1.||,||.y1.||,||.x3.||*> & ||.[x1,y1,x3].|| = |.w.| ) )
let z1 be Point of G; :: thesis: ( ||.[x1,y1,z1].|| = sqrt (((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.z1.|| ^2)) & ex w being Element of REAL 3 st
( w = <*||.x1.||,||.y1.||,||.z1.||*> & ||.[x1,y1,z1].|| = |.w.| ) )
consider v10 being Element of REAL 2 such that
A11: ( v10 = <*||.[x1,y1].||,||.z1.||*> & (prod_NORM ([:E,F:],G)) . ([x1,y1],z1) = |.v10.| ) by PRVECT_3:def 6;
consider v20 being Element of REAL 2 such that
A12: ( v20 = <*||.x1.||,||.y1.||*> & (prod_NORM (E,F)) . (x1,y1) = |.v20.| ) by PRVECT_3:def 6;
reconsider v1 = <*||.x1.||,||.y1.||,||.z1.||*> as Element of REAL 3 by FINSEQ_2:104;
A14: 0 <= Sum (sqr v20) by RVSUM_1:86;
A15: ||.[x1,y1].|| ^2 = Sum (sqr v20) by A14, SQUARE_1:def 2, A12
.= Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*> by A12, TOPREAL6:11
.= (||.x1.|| ^2) + (||.y1.|| ^2) by RVSUM_1:77 ;
A16: Sum (sqr v10) = Sum <*(||.[x1,y1].|| ^2),(||.z1.|| ^2)*> by TOPREAL6:11, A11
.= ((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.z1.|| ^2) by A15, RVSUM_1:77 ;
|.v10.| = |.v1.| by A16, BORSUK_7:17;
hence ( ||.[x1,y1,z1].|| = sqrt (((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.z1.|| ^2)) & ex w being Element of REAL 3 st
( w = <*||.x1.||,||.y1.||,||.z1.||*> & ||.[x1,y1,z1].|| = |.w.| ) ) by A11, A16; :: thesis: verum