let m, n be non zero Element of NAT ; :: thesis: ex f being Function of [:(REAL-NS m),(REAL-NS n):],(REAL-NS (m + n)) st
( f is one-to-one & f is onto & ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & ( for u, v being Point of [:(REAL-NS m),(REAL-NS n):] holds f . (u + v) = (f . u) + (f . v) ) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):]
for r being Real holds f . (r * u) = r * (f . u) ) & f . (0. [:(REAL-NS m),(REAL-NS n):]) = 0. (REAL-NS (m + n)) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):] holds ||.(f . u).|| = ||.u.|| ) )
consider f being Function of [:(REAL m),(REAL n):],(REAL (m + n)) such that
A1: ( ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & f is one-to-one & f is onto ) by Th14;
A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n & the carrier of (REAL-NS (m + n)) = REAL (m + n) ) by REAL_NS1:def 4;
reconsider f = f as Function of [:(REAL-NS m),(REAL-NS n):],(REAL-NS (m + n)) by A2;
take f ; :: thesis: ( f is one-to-one & f is onto & ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & ( for u, v being Point of [:(REAL-NS m),(REAL-NS n):] holds f . (u + v) = (f . u) + (f . v) ) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):]
for r being Real holds f . (r * u) = r * (f . u) ) & f . (0. [:(REAL-NS m),(REAL-NS n):]) = 0. (REAL-NS (m + n)) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):] holds ||.(f . u).|| = ||.u.|| ) )
A3: for u, v being Point of [:(REAL-NS m),(REAL-NS n):] holds f . (u + v) = (f . u) + (f . v)

proof

let u, v be Point of [:(REAL-NS m),(REAL-NS n):]; :: thesis: f . (u + v) = (f . u) + (f . v)
consider x1 being Point of (REAL-NS m), y1 being Point of (REAL-NS n) such that
A4: u = [x1,y1] by PRVECT_3:18;
consider x2 being Point of (REAL-NS m), y2 being Point of (REAL-NS n) such that
A5: v = [x2,y2] by PRVECT_3:18;
reconsider px1 = x1, px2 = x2 as Element of REAL m by REAL_NS1:def 4;
reconsider py1 = y1, py2 = y2 as Element of REAL n by REAL_NS1:def 4;
reconsider px1x2 = x1 + x2 as Element of REAL m by REAL_NS1:def 4;
reconsider py1y2 = y1 + y2 as Element of REAL n by REAL_NS1:def 4;
A6: f . u = f . (x1,y1) by A4
.= px1 ^ py1 by A1 ;
A7: f . v = f . (x2,y2) by A5
.= px2 ^ py2 by A1 ;
A8: f . (u + v) = f . ((x1 + x2),(y1 + y2)) by A4, A5, PRVECT_3:18
.= px1x2 ^ py1y2 by A1 ;
reconsider fu = f . u, fv = f . v, fuv = f . (u + v) as Element of REAL (m + n) by REAL_NS1:def 4;
A9: fu + fv = (f . u) + (f . v) by REAL_NS1:2;
A10: x1 + x2 = px1 + px2 by REAL_NS1:2;
A11: y1 + y2 = py1 + py2 by REAL_NS1:2;
A12: len (fu + fv) = m + n by CARD_1:def 7;
A13: ( len px1 = m & len px2 = m ) by CARD_1:def 7;
A14: ( len py1 = n & len py2 = n ) by CARD_1:def 7;
A15: len px1x2 = m by CARD_1:def 7;
A16: len py1y2 = n by CARD_1:def 7;
for i being Nat st 1 <= i & i <= len fuv holds
fuv . i = (fu + fv) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len fuv implies fuv . i = (fu + fv) . i )
assume A17: ( 1 <= i & i <= len fuv ) ; :: thesis: fuv . i = (fu + fv) . i

per cases ( i <= m or m < i ) ;

suppose A18: i <= m ; :: thesis: fuv . i = (fu + fv) . i

then i in Seg (len px1x2) by A15, A17;
then i in dom px1x2 by FINSEQ_1:def 3;
then A19: fuv . i = px1x2 . i by A8, FINSEQ_1:def 7;
A20: (fu + fv) . i = (fu . i) + (fv . i) by RVSUM_1:11;
i in Seg (len px1) by A13, A17, A18;
then i in dom px1 by FINSEQ_1:def 3;
then A21: fu . i = px1 . i by A6, FINSEQ_1:def 7;
i in Seg (len px2) by A13, A17, A18;
then i in dom px2 by FINSEQ_1:def 3;
then fv . i = px2 . i by A7, FINSEQ_1:def 7;
hence fuv . i = (fu + fv) . i by A10, A19, A20, A21, RVSUM_1:11; :: thesis: verum

end;

suppose m < i ; :: thesis: fuv . i = (fu + fv) . i

then not i in Seg (len px1x2) by A15, FINSEQ_1:1;
then A22: not i in dom px1x2 by FINSEQ_1:def 3;
i in Seg (len fuv) by A17;
then i in dom (px1x2 ^ py1y2) by A8, FINSEQ_1:def 3;
then consider j being Nat such that
A23: ( j in dom py1y2 & i = (len px1x2) + j ) by A22, FINSEQ_1:25;
A24: fuv . i = py1y2 . j by A8, A23, FINSEQ_1:def 7;
A25: (fu + fv) . i = (fu . i) + (fv . i) by RVSUM_1:11;
j in Seg (len py1y2) by A23, FINSEQ_1:def 3;
then j in dom py1 by A14, CARD_1:def 7, FINSEQ_1:def 3;
then A26: fu . i = py1 . j by A6, A13, A15, A23, FINSEQ_1:def 7;
j in Seg (len py2) by A16, A23, CARD_1:def 7, FINSEQ_1:def 3;
then j in dom py2 by FINSEQ_1:def 3;
then fv . i = py2 . j by A7, A23, A13, A15, FINSEQ_1:def 7;
hence fuv . i = (fu + fv) . i by A11, A24, A25, A26, RVSUM_1:11; :: thesis: verum

end;

end;

end;

hence f . (u + v) = (f . u) + (f . v) by A9, A12, FINSEQ_1:14, CARD_1:def 7; :: thesis: verum

end;

A28: for u being Point of [:(REAL-NS m),(REAL-NS n):]
for r being Real holds f . (r * u) = r * (f . u)

proof

let u be Point of [:(REAL-NS m),(REAL-NS n):]; :: thesis: for r being Real holds f . (r * u) = r * (f . u)
let r be Real; :: thesis: f . (r * u) = r * (f . u)
consider x1 being Point of (REAL-NS m), y1 being Point of (REAL-NS n) such that
A29: u = [x1,y1] by PRVECT_3:18;
reconsider px1 = x1, prx1 = r * x1 as Element of REAL m by REAL_NS1:def 4;
reconsider py1 = y1, pry1 = r * y1 as Element of REAL n by REAL_NS1:def 4;
A30: f . u = f . (x1,y1) by A29
.= px1 ^ py1 by A1 ;
A31: f . (r * u) = f . ((r * x1),(r * y1)) by A29, PRVECT_3:18
.= prx1 ^ pry1 by A1 ;
reconsider fu = f . u, fru = f . (r * u) as Element of REAL (m + n) by REAL_NS1:def 4;
A32: r * fu = r * (f . u) by REAL_NS1:3;
A33: r * x1 = r * px1 by REAL_NS1:3;
A34: r * y1 = r * py1 by REAL_NS1:3;
A35: len (r * fu) = m + n by CARD_1:def 7;
A36: len px1 = m by CARD_1:def 7;
A37: len py1 = n by CARD_1:def 7;
A38: len prx1 = m by CARD_1:def 7;
for i being Nat st 1 <= i & i <= len fru holds
fru . i = (r * fu) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len fru implies fru . i = (r * fu) . i )
assume A39: ( 1 <= i & i <= len fru ) ; :: thesis: fru . i = (r * fu) . i

per cases ( i <= m or m < i ) ;

suppose A40: i <= m ; :: thesis: fru . i = (r * fu) . i

then i in Seg (len prx1) by A38, A39;
then i in dom prx1 by FINSEQ_1:def 3;
then A41: fru . i = prx1 . i by A31, FINSEQ_1:def 7;
A42: (r * fu) . i = r * (fu . i) by RVSUM_1:44;
i in Seg (len px1) by A36, A39, A40;
then i in dom px1 by FINSEQ_1:def 3;
then fu . i = px1 . i by A30, FINSEQ_1:def 7;
hence fru . i = (r * fu) . i by A33, A41, A42, RVSUM_1:44; :: thesis: verum

end;

suppose m < i ; :: thesis: fru . i = (r * fu) . i

then not i in Seg (len prx1) by A38, FINSEQ_1:1;
then A43: not i in dom prx1 by FINSEQ_1:def 3;
i in Seg (len fru) by A39;
then i in dom (prx1 ^ pry1) by A31, FINSEQ_1:def 3;
then consider j being Nat such that
A44: ( j in dom pry1 & i = (len prx1) + j ) by A43, FINSEQ_1:25;
A45: fru . i = pry1 . j by A44, A31, FINSEQ_1:def 7;
A46: (r * fu) . i = r * (fu . i) by RVSUM_1:44;
j in Seg (len pry1) by A44, FINSEQ_1:def 3;
then j in dom py1 by A37, CARD_1:def 7, FINSEQ_1:def 3;
then fu . i = py1 . j by A30, A36, A38, A44, FINSEQ_1:def 7;
hence fru . i = (r * fu) . i by A34, A45, A46, RVSUM_1:44; :: thesis: verum

end;

end;

end;

hence f . (r * u) = r * (f . u) by A32, A35, FINSEQ_1:14, CARD_1:def 7; :: thesis: verum

end;

0. [:(REAL-NS m),(REAL-NS n):] = (0. [:(REAL-NS m),(REAL-NS n):]) + (0. [:(REAL-NS m),(REAL-NS n):]) by RLVECT_1:4;
then A47: ((f . (0. [:(REAL-NS m),(REAL-NS n):])) + (f . (0. [:(REAL-NS m),(REAL-NS n):]))) - (f . (0. [:(REAL-NS m),(REAL-NS n):])) = (f . (0. [:(REAL-NS m),(REAL-NS n):])) - (f . (0. [:(REAL-NS m),(REAL-NS n):])) by A3
.= 0. (REAL-NS (m + n)) by RLVECT_1:15 ;
A48: ((f . (0. [:(REAL-NS m),(REAL-NS n):])) + (f . (0. [:(REAL-NS m),(REAL-NS n):]))) - (f . (0. [:(REAL-NS m),(REAL-NS n):])) = (f . (0. [:(REAL-NS m),(REAL-NS n):])) + ((f . (0. [:(REAL-NS m),(REAL-NS n):])) - (f . (0. [:(REAL-NS m),(REAL-NS n):]))) by RLVECT_1:28
.= (f . (0. [:(REAL-NS m),(REAL-NS n):])) + (0. (REAL-NS (m + n))) by RLVECT_1:15
.= f . (0. [:(REAL-NS m),(REAL-NS n):]) by RLVECT_1:4 ;
for u being Point of [:(REAL-NS m),(REAL-NS n):] holds ||.(f . u).|| = ||.u.||

proof

let u be Point of [:(REAL-NS m),(REAL-NS n):]; :: thesis: ||.(f . u).|| = ||.u.||
consider x1 being Point of (REAL-NS m), y1 being Point of (REAL-NS n) such that
A50: u = [x1,y1] by PRVECT_3:18;
reconsider px1 = x1 as Element of REAL m by REAL_NS1:def 4;
reconsider py1 = y1 as Element of REAL n by REAL_NS1:def 4;
A51: f . u = f . (x1,y1) by A50
.= px1 ^ py1 by A1 ;
consider v being Element of REAL 2 such that
A52: ( v = <*||.x1.||,||.y1.||*> & ||.u.|| = |.v.| ) by A50, PRVECT_3:18;
reconsider fu = f . u as Element of REAL (m + n) by REAL_NS1:def 4;
A53: ||.(f . u).|| = |.fu.| by REAL_NS1:1;
( sqr px1 is Element of REAL m & ( for k being Nat st k in Seg m holds
0 <= (sqr px1) . k ) )

proof

thus sqr px1 is Element of REAL m ; :: thesis: for k being Nat st k in Seg m holds
0 <= (sqr px1) . k
let k be Nat; :: thesis: ( k in Seg m implies 0 <= (sqr px1) . k )
assume k in Seg m ; :: thesis: 0 <= (sqr px1) . k
(sqr px1) . k = (px1 . k) ^2 by VALUED_1:11
.= (px1 . k) * (px1 . k) ;
hence 0 <= (sqr px1) . k by XREAL_1:63; :: thesis: verum

end;

then A54: ( |.px1.| = sqrt (Sum (sqr px1)) & 0 <= Sum (sqr px1) ) by REAL_NS1:7;
( sqr py1 is Element of REAL n & ( for k being Nat st k in Seg n holds
0 <= (sqr py1) . k ) )

proof

thus sqr py1 is Element of REAL n ; :: thesis: for k being Nat st k in Seg n holds
0 <= (sqr py1) . k
let k be Nat; :: thesis: ( k in Seg n implies 0 <= (sqr py1) . k )
(sqr py1) . k = (py1 . k) ^2 by VALUED_1:11
.= (py1 . k) * (py1 . k) ;
hence ( k in Seg n implies 0 <= (sqr py1) . k ) by XREAL_1:63; :: thesis: verum

end;

then ( |.py1.| = sqrt (Sum (sqr py1)) & 0 <= Sum (sqr py1) ) by REAL_NS1:7;
then A55: |.py1.| ^2 = Sum (sqr py1) by SQUARE_1:def 2;
( sqr (px1 ^ py1) is Element of REAL (m + n) & ( for k being Nat st k in Seg (m + n) holds
0 <= (sqr (px1 ^ py1)) . k ) )

proof

sqr fu is Element of REAL (m + n) ;
hence sqr (px1 ^ py1) is Element of REAL (m + n) by A51; :: thesis: for k being Nat st k in Seg (m + n) holds
0 <= (sqr (px1 ^ py1)) . k
let k be Nat; :: thesis: ( k in Seg (m + n) implies 0 <= (sqr (px1 ^ py1)) . k )
(sqr (px1 ^ py1)) . k = ((px1 ^ py1) . k) ^2 by VALUED_1:11
.= ((px1 ^ py1) . k) * ((px1 ^ py1) . k) ;
hence ( k in Seg (m + n) implies 0 <= (sqr (px1 ^ py1)) . k ) by XREAL_1:63; :: thesis: verum

end;

then A56: ( |.(px1 ^ py1).| = sqrt (Sum (sqr (px1 ^ py1))) & 0 <= Sum (sqr (px1 ^ py1)) ) by REAL_NS1:7;
reconsider ww = v as Point of (TOP-REAL 2) by EUCLID:22;
A57: ww `1 = ||.x1.|| by A52;
A58: ww `2 = ||.y1.|| by A52;
|.fu.| ^2 = Sum (sqr (px1 ^ py1)) by A51, A56, SQUARE_1:def 2
.= Sum ((sqr px1) ^ (sqr py1)) by TOPREAL7:10
.= (Sum (sqr px1)) + (Sum (sqr py1)) by RVSUM_1:75
.= (|.px1.| ^2) + (|.py1.| ^2) by A54, A55, SQUARE_1:def 2
.= (||.x1.|| ^2) + (|.py1.| ^2) by REAL_NS1:1
.= (||.x1.|| ^2) + (||.y1.|| ^2) by REAL_NS1:1
.= |.v.| ^2 by A57, A58, JGRAPH_1:29 ;
then sqrt (|.fu.| ^2) = |.v.| by SQUARE_1:22;
hence ||.(f . u).|| = ||.u.|| by A52, A53, SQUARE_1:22; :: thesis: verum

end;

hence ( f is one-to-one & f is onto & ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & ( for u, v being Point of [:(REAL-NS m),(REAL-NS n):] holds f . (u + v) = (f . u) + (f . v) ) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):]
for r being Real holds f . (r * u) = r * (f . u) ) & f . (0. [:(REAL-NS m),(REAL-NS n):]) = 0. (REAL-NS (m + n)) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):] holds ||.(f . u).|| = ||.u.|| ) ) by A1, A3, A28, A47, A48, REAL_NS1:def 4; :: thesis: verum