let X, Y, Z be RealNormSpace; :: thesis: ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y

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

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

A1: the carrier of [:X,Y,Z:] = [: the carrier of X, the carrier of Y, the carrier of Z:] ;

reconsider X0 = X, Y0 = Y, Z0 = Z as RealLinearSpace ;

consider I0 being Function of [:X0,Y0,Z0:],(product <*X0,Y0,Z0*>) such that

A2: ( I0 is one-to-one & I0 is onto & ( for x being Point of X

for y being Point of Y

for z being Point of Z holds I0 . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X0,Y0,Z0:] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:X0,Y0,Z0:]

for r being Real holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0,Z0*>) = I0 . (0. [:X0,Y0,Z0:]) ) by Th11;

A3: product <*X,Y,Z*> = NORMSTR(# (product (carr <*X,Y,Z*>)),(zeros <*X,Y,Z*>),[:(addop <*X,Y,Z*>):],[:(multop <*X,Y,Z*>):],(productnorm <*X,Y,Z*>) #) by PRVECT_2:6;

then reconsider I = I0 as Function of [:X,Y,Z:],(product <*X,Y,Z*>) ;

take I ; :: thesis: ( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y

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

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

A4a: for g1, g2 being Point of [:X0,Y0:]

for f1, f2 being Point of Z0 holds (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

for g being Point of [:X0,Y0:]

for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

for y being Point of Y

for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) ) by A2, A3; :: thesis: ( ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||

( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y

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

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

A1: the carrier of [:X,Y,Z:] = [: the carrier of X, the carrier of Y, the carrier of Z:] ;

reconsider X0 = X, Y0 = Y, Z0 = Z as RealLinearSpace ;

consider I0 being Function of [:X0,Y0,Z0:],(product <*X0,Y0,Z0*>) such that

A2: ( I0 is one-to-one & I0 is onto & ( for x being Point of X

for y being Point of Y

for z being Point of Z holds I0 . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X0,Y0,Z0:] holds I0 . (v + w) = (I0 . v) + (I0 . w) ) & ( for v being Point of [:X0,Y0,Z0:]

for r being Real holds I0 . (r * v) = r * (I0 . v) ) & 0. (product <*X0,Y0,Z0*>) = I0 . (0. [:X0,Y0,Z0:]) ) by Th11;

A3: product <*X,Y,Z*> = NORMSTR(# (product (carr <*X,Y,Z*>)),(zeros <*X,Y,Z*>),[:(addop <*X,Y,Z*>):],[:(multop <*X,Y,Z*>):],(productnorm <*X,Y,Z*>) #) by PRVECT_2:6;

then reconsider I = I0 as Function of [:X,Y,Z:],(product <*X,Y,Z*>) ;

take I ; :: thesis: ( I is one-to-one & I is onto & ( for x being Point of X

for y being Point of Y

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

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

A4a: for g1, g2 being Point of [:X0,Y0:]

for f1, f2 being Point of Z0 holds (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

proof

A5a:
for r being Real
let g1, g2 be Point of [:X0,Y0:]; :: thesis: for f1, f2 being Point of Z0 holds (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

let f1, f2 be Point of Z0; :: thesis: (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

reconsider gg1 = g1, gg2 = g2 as Point of [:X,Y:] ;

reconsider ff1 = f1, ff2 = f2 as Point of Z ;

thus (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(gg1 + gg2),(ff1 + ff2)] by PRVECT_3:def 1

.= [(g1 + g2),(f1 + f2)] ; :: thesis: verum

end;let f1, f2 be Point of Z0; :: thesis: (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]

reconsider gg1 = g1, gg2 = g2 as Point of [:X,Y:] ;

reconsider ff1 = f1, ff2 = f2 as Point of Z ;

thus (prod_ADD ([:X,Y:],Z)) . ([g1,f1],[g2,f2]) = [(gg1 + gg2),(ff1 + ff2)] by PRVECT_3:def 1

.= [(g1 + g2),(f1 + f2)] ; :: thesis: verum

for g being Point of [:X0,Y0:]

for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

proof

thus
( I is one-to-one & I is onto & ( for x being Point of X
let r be Real; :: thesis: for g being Point of [:X0,Y0:]

for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

let g be Point of [:X0,Y0:]; :: thesis: for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

let f be Point of Z0; :: thesis: (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

reconsider gg = g as Point of [:X,Y:] ;

reconsider ff = f as Point of Z ;

thus (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * gg),(r * ff)] by PRVECT_3:def 2

.= [(r * g),(r * f)] ; :: thesis: verum

end;for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

let g be Point of [:X0,Y0:]; :: thesis: for f being Point of Z0 holds (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

let f be Point of Z0; :: thesis: (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * g),(r * f)]

reconsider gg = g as Point of [:X,Y:] ;

reconsider ff = f as Point of Z ;

thus (prod_MLT ([:X,Y:],Z)) . (r,[g,f]) = [(r * gg),(r * ff)] by PRVECT_3:def 2

.= [(r * g),(r * f)] ; :: thesis: verum

for y being Point of Y

for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) ) by A2, A3; :: thesis: ( ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

hereby :: thesis: ( ( for v being Point of [:X,Y,Z:]

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

let v, w be Point of [:X,Y,Z:]; :: thesis: I . (v + w) = (I . v) + (I . w)

reconsider v0 = v, w0 = w as Point of [:X0,Y0,Z0:] ;

thus I . (v + w) = I0 . (v0 + w0) by A4a, PRVECT_3:def 1

.= (I0 . v0) + (I0 . w0) by A2

.= (I . v) + (I . w) by A3 ; :: thesis: verum

end;reconsider v0 = v, w0 = w as Point of [:X0,Y0,Z0:] ;

thus I . (v + w) = I0 . (v0 + w0) by A4a, PRVECT_3:def 1

.= (I0 . v0) + (I0 . w0) by A2

.= (I . v) + (I . w) by A3 ; :: thesis: verum

hereby :: thesis: ( 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )

thus
0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:])
by A2, A3; :: thesis: for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||let v be Point of [:X,Y,Z:]; :: thesis: for r being Real holds I . (r * v) = r * (I . v)

let r be Real; :: thesis: I . (r * v) = r * (I . v)

reconsider v0 = v as Point of [:X0,Y0,Z0:] ;

thus I . (r * v) = I0 . (r * v0) by A5a, PRVECT_3:def 2

.= r * (I0 . v0) by A2

.= r * (I . v) by A3 ; :: thesis: verum

end;let r be Real; :: thesis: I . (r * v) = r * (I . v)

reconsider v0 = v as Point of [:X0,Y0,Z0:] ;

thus I . (r * v) = I0 . (r * v0) by A5a, PRVECT_3:def 2

.= r * (I0 . v0) by A2

.= r * (I . v) by A3 ; :: thesis: verum

for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||

proof

hence
for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.||
; :: thesis: verum
let v be Point of [:X,Y,Z:]; :: thesis: ||.(I . v).|| = ||.v.||

consider x1 being Point of X, y1 being Point of Y, z1 being Point of Z such that

A6: v = [x1,y1,z1] by Lm1, A1;

consider v10 being Element of REAL 2 such that

A7: ( v10 = <*||.[x1,y1].||,||.z1.||*> & (prod_NORM ([:X,Y:],Z)) . ([x1,y1],z1) = |.v10.| ) by PRVECT_3:def 6;

consider v20 being Element of REAL 2 such that

A8: ( v20 = <*||.x1.||,||.y1.||*> & (prod_NORM (X,Y)) . (x1,y1) = |.v20.| ) by PRVECT_3:def 6;

reconsider v1 = <*||.x1.||,||.y1.||,||.z1.||*> as Element of REAL 3 by FINSEQ_2:104;

A10: 0 <= Sum (sqr v20) by RVSUM_1:86;

A11: ||.[x1,y1].|| ^2 = Sum (sqr v20) by A10, SQUARE_1:def 2, A8

.= Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*> by A8, TOPREAL6:11

.= (||.x1.|| ^2) + (||.y1.|| ^2) by RVSUM_1:77 ;

A12: Sum (sqr v10) = Sum <*(||.[x1,y1].|| ^2),(||.z1.|| ^2)*> by TOPREAL6:11, A7

.= ((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.z1.|| ^2) by A11, RVSUM_1:77

.= Sum (sqr v1) by BORSUK_7:17 ;

A13: |.v10.| = |.v1.| by A12;

A14: I . v = I . (x1,y1,z1) by A6

.= <*x1,y1,z1*> by A2 ;

reconsider Iv = I . v as Element of product (carr <*X,Y,Z*>) by A3;

A15: ( <*x1,y1,z1*> . 1 = x1 & <*x1,y1,z1*> . 2 = y1 & <*x1,y1,z1*> . 3 = z1 ) by FINSEQ_1:45;

dom <*X,Y,Z*> = Seg (len <*X,Y,Z*>) by FINSEQ_1:def 3

.= {1,2,3} by FINSEQ_1:45, FINSEQ_3:1 ;

then reconsider j1 = 1, j2 = 2, j3 = 3 as Element of dom <*X,Y,Z*> by ENUMSET1:def 1;

A17: (normsequence (<*X,Y,Z*>,Iv)) . j1 = the normF of (<*X,Y,Z*> . j1) . (Iv . j1) by PRVECT_2:def 11

.= ||.x1.|| by A14, A15, FINSEQ_1:45 ;

A18: (normsequence (<*X,Y,Z*>,Iv)) . j2 = the normF of (<*X,Y,Z*> . j2) . (Iv . j2) by PRVECT_2:def 11

.= ||.y1.|| by A14, A15, FINSEQ_1:45 ;

A19: (normsequence (<*X,Y,Z*>,Iv)) . j3 = the normF of (<*X,Y,Z*> . j3) . (Iv . j3) by PRVECT_2:def 11

.= ||.z1.|| by A14, A15, FINSEQ_1:45 ;

len (normsequence (<*X,Y,Z*>,Iv)) = len <*X,Y,Z*> by PRVECT_2:def 11

.= 3 by FINSEQ_1:45 ;

then normsequence (<*X,Y,Z*>,Iv) = v1 by A17, A18, A19, FINSEQ_1:45;

hence ||.(I . v).|| = ||.v.|| by A13, A7, A6, A3, PRVECT_2:def 12; :: thesis: verum

end;consider x1 being Point of X, y1 being Point of Y, z1 being Point of Z such that

A6: v = [x1,y1,z1] by Lm1, A1;

consider v10 being Element of REAL 2 such that

A7: ( v10 = <*||.[x1,y1].||,||.z1.||*> & (prod_NORM ([:X,Y:],Z)) . ([x1,y1],z1) = |.v10.| ) by PRVECT_3:def 6;

consider v20 being Element of REAL 2 such that

A8: ( v20 = <*||.x1.||,||.y1.||*> & (prod_NORM (X,Y)) . (x1,y1) = |.v20.| ) by PRVECT_3:def 6;

reconsider v1 = <*||.x1.||,||.y1.||,||.z1.||*> as Element of REAL 3 by FINSEQ_2:104;

A10: 0 <= Sum (sqr v20) by RVSUM_1:86;

A11: ||.[x1,y1].|| ^2 = Sum (sqr v20) by A10, SQUARE_1:def 2, A8

.= Sum <*(||.x1.|| ^2),(||.y1.|| ^2)*> by A8, TOPREAL6:11

.= (||.x1.|| ^2) + (||.y1.|| ^2) by RVSUM_1:77 ;

A12: Sum (sqr v10) = Sum <*(||.[x1,y1].|| ^2),(||.z1.|| ^2)*> by TOPREAL6:11, A7

.= ((||.x1.|| ^2) + (||.y1.|| ^2)) + (||.z1.|| ^2) by A11, RVSUM_1:77

.= Sum (sqr v1) by BORSUK_7:17 ;

A13: |.v10.| = |.v1.| by A12;

A14: I . v = I . (x1,y1,z1) by A6

.= <*x1,y1,z1*> by A2 ;

reconsider Iv = I . v as Element of product (carr <*X,Y,Z*>) by A3;

A15: ( <*x1,y1,z1*> . 1 = x1 & <*x1,y1,z1*> . 2 = y1 & <*x1,y1,z1*> . 3 = z1 ) by FINSEQ_1:45;

dom <*X,Y,Z*> = Seg (len <*X,Y,Z*>) by FINSEQ_1:def 3

.= {1,2,3} by FINSEQ_1:45, FINSEQ_3:1 ;

then reconsider j1 = 1, j2 = 2, j3 = 3 as Element of dom <*X,Y,Z*> by ENUMSET1:def 1;

A17: (normsequence (<*X,Y,Z*>,Iv)) . j1 = the normF of (<*X,Y,Z*> . j1) . (Iv . j1) by PRVECT_2:def 11

.= ||.x1.|| by A14, A15, FINSEQ_1:45 ;

A18: (normsequence (<*X,Y,Z*>,Iv)) . j2 = the normF of (<*X,Y,Z*> . j2) . (Iv . j2) by PRVECT_2:def 11

.= ||.y1.|| by A14, A15, FINSEQ_1:45 ;

A19: (normsequence (<*X,Y,Z*>,Iv)) . j3 = the normF of (<*X,Y,Z*> . j3) . (Iv . j3) by PRVECT_2:def 11

.= ||.z1.|| by A14, A15, FINSEQ_1:45 ;

len (normsequence (<*X,Y,Z*>,Iv)) = len <*X,Y,Z*> by PRVECT_2:def 11

.= 3 by FINSEQ_1:45 ;

then normsequence (<*X,Y,Z*>,Iv) = v1 by A17, A18, A19, FINSEQ_1:45;

hence ||.(I . v).|| = ||.v.|| by A13, A7, A6, A3, PRVECT_2:def 12; :: thesis: verum