let E, F, G be RealNormSpace; :: thesis: ( ( for x being set holds

( x is Point of (product <*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. (product <*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 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

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*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| ) ) ) )

consider I being Function of [:E,F,G:],(product <*E,F,G*>) such that

A1: ( I is one-to-one & I is onto & ( for x being Point of E

for y being Point of F

for z being Point of G holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:E,F,G:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:E,F,G:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*E,F,G*>) = I . (0. [:E,F,G:]) & ( for v being Point of [:E,F,G:] holds ||.(I . v).|| = ||.v.|| ) ) by Th15;

thus for x being set holds

( x is Point of (product <*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. (product <*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 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

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*>.|| = 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, 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)*> :: thesis: ( 0. (product <*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 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

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*>.|| = 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 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

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*>.|| = 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 x2 be Point of F; :: thesis: 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 x3 be Point of G; :: thesis: ( ||.<*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.| ) )

A16: I . [x1,x2,x3] = I . (x1,x2,x3)

.= <*x1,x2,x3*> by A1 ;

||.[x1,x2,x3].|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) by Th14;

hence ||.<*x1,x2,x3*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) by A1, A16; :: thesis: ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| )

consider w being Element of REAL 3 such that

A17: ( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.[x1,x2,x3].|| = |.w.| ) by Th14;

take w ; :: thesis: ( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| )

thus w = <*||.x1.||,||.x2.||,||.x3.||*> by A17; :: thesis: ||.<*x1,x2,x3*>.|| = |.w.|

thus ||.<*x1,x2,x3*>.|| = |.w.| by A1, A17, A16; :: thesis: verum

( x is Point of (product <*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. (product <*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 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

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*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| ) ) ) )

consider I being Function of [:E,F,G:],(product <*E,F,G*>) such that

A1: ( I is one-to-one & I is onto & ( for x being Point of E

for y being Point of F

for z being Point of G holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:E,F,G:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:E,F,G:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*E,F,G*>) = I . (0. [:E,F,G:]) & ( for v being Point of [:E,F,G:] holds ||.(I . v).|| = ||.v.|| ) ) by Th15;

thus for x being set holds

( x is Point of (product <*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. (product <*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 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

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*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| ) ) ) )

proof

thus A7:
for x1, y1 being Point of E
let y be set ; :: thesis: ( y is Point of (product <*E,F,G*>) iff ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*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 y = <*x1,x2,x3*> implies y is Point of (product <*E,F,G*>) )

thus
( ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*> implies y is Point of (product <*E,F,G*>) )
; :: thesis: verumassume
y is Point of (product <*E,F,G*>)
; :: thesis: ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>

then y in the carrier of (product <*E,F,G*>) ;

then y in rng I by A1, FUNCT_2:def 3;

then consider x being Element of the carrier of [:E,F,G:] such that

A3: y = I . x by FUNCT_2:113;

consider x1 being Point of E, x2 being Point of F, x3 being Point of G such that

A4: x = [x1,x2,x3] by Th14;

take x1 = x1; :: thesis: ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>

take x2 = x2; :: thesis: ex x3 being Point of G st y = <*x1,x2,x3*>

take x3 = x3; :: thesis: y = <*x1,x2,x3*>

I . (x1,x2,x3) = <*x1,x2,x3*> by A1;

hence y = <*x1,x2,x3*> by A3, A4; :: thesis: verum

end;then y in the carrier of (product <*E,F,G*>) ;

then y in rng I by A1, FUNCT_2:def 3;

then consider x being Element of the carrier of [:E,F,G:] such that

A3: y = I . x by FUNCT_2:113;

consider x1 being Point of E, x2 being Point of F, x3 being Point of G such that

A4: x = [x1,x2,x3] by Th14;

take x1 = x1; :: thesis: ex x2 being Point of F ex x3 being Point of G st y = <*x1,x2,x3*>

take x2 = x2; :: thesis: ex x3 being Point of G st y = <*x1,x2,x3*>

take x3 = x3; :: thesis: y = <*x1,x2,x3*>

I . (x1,x2,x3) = <*x1,x2,x3*> by A1;

hence y = <*x1,x2,x3*> by A3, A4; :: thesis: verum

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)*> :: thesis: ( 0. (product <*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 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

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*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| ) ) ) )

proof

thus A11:
0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*>
:: thesis: ( ( for x1 being Point of E
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)*>

A9: [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by Th14;

A10: I . ((x1 + y1),(x2 + y2),(x3 + y3)) = <*(x1 + y1),(x2 + y2),(x3 + y3)*> by A1;

( I . (x1,x2,x3) = <*x1,x2,x3*> & I . (y1,y2,y3) = <*y1,y2,y3*> ) by A1;

hence <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> by A1, A9, A10; :: 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)*>

A9: [x1,x2,x3] + [y1,y2,y3] = [(x1 + y1),(x2 + y2),(x3 + y3)] by Th14;

A10: I . ((x1 + y1),(x2 + y2),(x3 + y3)) = <*(x1 + y1),(x2 + y2),(x3 + y3)*> by A1;

( I . (x1,x2,x3) = <*x1,x2,x3*> & I . (y1,y2,y3) = <*y1,y2,y3*> ) by A1;

hence <*x1,x2,x3*> + <*y1,y2,y3*> = <*(x1 + y1),(x2 + y2),(x3 + y3)*> by A1, A9, A10; :: thesis: verum

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

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*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) & ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| ) ) ) )

proof

I . ((0. E),(0. F),(0. G)) = <*(0. E),(0. F),(0. G)*>
by A1;

hence 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> by A1; :: thesis: verum

end;hence 0. (product <*E,F,G*>) = <*(0. E),(0. F),(0. G)*> by A1; :: thesis: verum

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

<*x1,x2,x3*> + <*(- x1),(- x2),(- x3)*> = <*(x1 + (- x1)),(x2 + (- x2)),(x3 + (- x3))*> by A7

.= <*(0. E),(x2 + (- x2)),(x3 + (- x3))*> by RLVECT_1:def 10

.= <*(0. E),(0. F),(x3 + (- x3))*> by RLVECT_1:def 10

.= 0. (product <*E,F,G*>) by A11, RLVECT_1:def 10 ;

hence - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> by RLVECT_1:def 10; :: 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)*>

<*x1,x2,x3*> + <*(- x1),(- x2),(- x3)*> = <*(x1 + (- x1)),(x2 + (- x2)),(x3 + (- x3))*> by A7

.= <*(0. E),(x2 + (- x2)),(x3 + (- x3))*> by RLVECT_1:def 10

.= <*(0. E),(0. F),(x3 + (- x3))*> by RLVECT_1:def 10

.= 0. (product <*E,F,G*>) by A11, RLVECT_1:def 10 ;

hence - <*x1,x2,x3*> = <*(- x1),(- x2),(- x3)*> by RLVECT_1:def 10; :: 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

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

A14: <*x1,x2,x3*> = I . (x1,x2,x3) by A1;

I . (a * [x1,x2,x3]) = I . ((a * x1),(a * x2),(a * x3)) by Th14

.= <*(a * x1),(a * x2),(a * x3)*> by A1 ;

hence a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> by A14, A1; :: 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)*>

A14: <*x1,x2,x3*> = I . (x1,x2,x3) by A1;

I . (a * [x1,x2,x3]) = I . ((a * x1),(a * x2),(a * x3)) by Th14

.= <*(a * x1),(a * x2),(a * x3)*> by A1 ;

hence a * <*x1,x2,x3*> = <*(a * x1),(a * x2),(a * x3)*> by A14, A1; :: 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 x2 be Point of F; :: thesis: 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 x3 be Point of G; :: thesis: ( ||.<*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.| ) )

A16: I . [x1,x2,x3] = I . (x1,x2,x3)

.= <*x1,x2,x3*> by A1 ;

||.[x1,x2,x3].|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) by Th14;

hence ||.<*x1,x2,x3*>.|| = sqrt (((||.x1.|| ^2) + (||.x2.|| ^2)) + (||.x3.|| ^2)) by A1, A16; :: thesis: ex w being Element of REAL 3 st

( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| )

consider w being Element of REAL 3 such that

A17: ( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.[x1,x2,x3].|| = |.w.| ) by Th14;

take w ; :: thesis: ( w = <*||.x1.||,||.x2.||,||.x3.||*> & ||.<*x1,x2,x3*>.|| = |.w.| )

thus w = <*||.x1.||,||.x2.||,||.x3.||*> by A17; :: thesis: ||.<*x1,x2,x3*>.|| = |.w.|

thus ||.<*x1,x2,x3*>.|| = |.w.| by A1, A17, A16; :: thesis: verum