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.| ) ) ) )

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.| ) ) ) )

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

( 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] )

end;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:] )

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: verumassume
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;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

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.| ) ) ) )

thus
0. [:E,F,G:] = [(0. E),(0. F),(0. G)]
; :: thesis: ( ( for x1 being Point of Efor 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;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

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;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

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 Ffor 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;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

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