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

proof

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

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

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

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: verum

end;

thus A7: 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)*> :: 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

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;

thus A11: 0. (product <*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 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;

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

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;

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

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