let X, Y be RealLinearSpace; :: thesis: for n being Nat

for x being FinSequence of the carrier of X

for y being FinSequence of the carrier of Y

for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n & len y = n & len z = n & ( for i being Nat st i in Seg n holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

defpred S_{1}[ Nat] means for x being FinSequence of the carrier of X

for y being FinSequence of the carrier of Y

for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = $1 & len y = $1 & len z = $1 & ( for i being Nat st i in Seg $1 holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)];

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A26, A1); :: thesis: verum

for x being FinSequence of the carrier of X

for y being FinSequence of the carrier of Y

for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n & len y = n & len z = n & ( for i being Nat st i in Seg n holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

defpred S

for y being FinSequence of the carrier of Y

for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = $1 & len y = $1 & len z = $1 & ( for i being Nat st i in Seg $1 holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)];

A1: for n being Nat st S

S

proof

A26:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A2: S

thus S

proof

let x be FinSequence of the carrier of X; :: thesis: for y being FinSequence of the carrier of Y

for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let y be FinSequence of the carrier of Y; :: thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); :: thesis: ( len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )

assume that

A3: len x = n + 1 and

A4: len y = n + 1 and

A5: len z = n + 1 and

A6: for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ; :: thesis: Sum z = [(Sum x),(Sum y)]

A7: 0 + n <= 1 + n by XREAL_1:6;

then A8: len (y | n) = n by A4, FINSEQ_1:59;

A9: Seg n c= Seg (n + 1) by A7, FINSEQ_1:5;

A10: for i being Nat st i in Seg n holds

(z | n) . i = [((x | n) . i),((y | n) . i)]

( x /. i = x . i & y /. i = y . i & z /. i = z . i )

then A19: y /. (n + 1) = y . (n + 1) by A15;

z | n = z | (Seg n) by FINSEQ_1:def 15;

then z = (z | n) ^ <*(z . (n + 1))*> by A5, FINSEQ_3:55;

then z = (z | n) ^ <*(z /. (n + 1))*> by A15, A18;

then A20: Sum z = (Sum (z | n)) + (Sum <*(z /. (n + 1))*>) by RLVECT_1:41

.= (Sum (z | n)) + (z /. (n + 1)) by RLVECT_1:44 ;

y | n = y | (Seg n) by FINSEQ_1:def 15;

then y = (y | n) ^ <*(y . (n + 1))*> by A4, FINSEQ_3:55;

then y = (y | n) ^ <*(y /. (n + 1))*> by A15, A18;

then A21: Sum y = (Sum (y | n)) + (Sum <*(y /. (n + 1))*>) by RLVECT_1:41

.= (Sum (y | n)) + (y /. (n + 1)) by RLVECT_1:44 ;

x | n = x | (Seg n) by FINSEQ_1:def 15;

then x = (x | n) ^ <*(x . (n + 1))*> by A3, FINSEQ_3:55;

then x = (x | n) ^ <*(x /. (n + 1))*> by A15, A18;

then A22: Sum x = (Sum (x | n)) + (Sum <*(x /. (n + 1))*>) by RLVECT_1:41

.= (Sum (x | n)) + (x /. (n + 1)) by RLVECT_1:44 ;

A23: z /. (n + 1) = z . (n + 1) by A15, A18;

x /. (n + 1) = x . (n + 1) by A15, A18;

then A24: z /. (n + 1) = [(x /. (n + 1)),(y /. (n + 1))] by A6, A19, A23, FINSEQ_1:4;

A25: len (z | n) = n by A5, A7, FINSEQ_1:59;

len (x | n) = n by A3, A7, FINSEQ_1:59;

then Sum (z | n) = [(Sum (x | n)),(Sum (y | n))] by A2, A8, A25, A10;

hence Sum z = [(Sum x),(Sum y)] by A24, A22, A21, A20, Def1; :: thesis: verum

end;for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let y be FinSequence of the carrier of Y; :: thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); :: thesis: ( len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )

assume that

A3: len x = n + 1 and

A4: len y = n + 1 and

A5: len z = n + 1 and

A6: for i being Nat st i in Seg (n + 1) holds

z . i = [(x . i),(y . i)] ; :: thesis: Sum z = [(Sum x),(Sum y)]

A7: 0 + n <= 1 + n by XREAL_1:6;

then A8: len (y | n) = n by A4, FINSEQ_1:59;

A9: Seg n c= Seg (n + 1) by A7, FINSEQ_1:5;

A10: for i being Nat st i in Seg n holds

(z | n) . i = [((x | n) . i),((y | n) . i)]

proof

A15:
for i being Element of NAT st i in Seg (n + 1) holds
let i be Nat; :: thesis: ( i in Seg n implies (z | n) . i = [((x | n) . i),((y | n) . i)] )

assume A11: i in Seg n ; :: thesis: (z | n) . i = [((x | n) . i),((y | n) . i)]

then A12: i <= n by FINSEQ_1:1;

then A13: (y | n) . i = y . i by FINSEQ_3:112;

A14: (z | n) . i = z . i by A12, FINSEQ_3:112;

(x | n) . i = x . i by A12, FINSEQ_3:112;

hence (z | n) . i = [((x | n) . i),((y | n) . i)] by A6, A9, A11, A13, A14; :: thesis: verum

end;assume A11: i in Seg n ; :: thesis: (z | n) . i = [((x | n) . i),((y | n) . i)]

then A12: i <= n by FINSEQ_1:1;

then A13: (y | n) . i = y . i by FINSEQ_3:112;

A14: (z | n) . i = z . i by A12, FINSEQ_3:112;

(x | n) . i = x . i by A12, FINSEQ_3:112;

hence (z | n) . i = [((x | n) . i),((y | n) . i)] by A6, A9, A11, A13, A14; :: thesis: verum

( x /. i = x . i & y /. i = y . i & z /. i = z . i )

proof

A18:
n + 1 in Seg (n + 1)
by FINSEQ_1:4;
let i be Element of NAT ; :: thesis: ( i in Seg (n + 1) implies ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) )

assume A16: i in Seg (n + 1) ; :: thesis: ( x /. i = x . i & y /. i = y . i & z /. i = z . i )

then A17: i <= n + 1 by FINSEQ_1:1;

1 <= i by A16, FINSEQ_1:1;

hence ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) by A3, A4, A5, A17, FINSEQ_4:15; :: thesis: verum

end;assume A16: i in Seg (n + 1) ; :: thesis: ( x /. i = x . i & y /. i = y . i & z /. i = z . i )

then A17: i <= n + 1 by FINSEQ_1:1;

1 <= i by A16, FINSEQ_1:1;

hence ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) by A3, A4, A5, A17, FINSEQ_4:15; :: thesis: verum

then A19: y /. (n + 1) = y . (n + 1) by A15;

z | n = z | (Seg n) by FINSEQ_1:def 15;

then z = (z | n) ^ <*(z . (n + 1))*> by A5, FINSEQ_3:55;

then z = (z | n) ^ <*(z /. (n + 1))*> by A15, A18;

then A20: Sum z = (Sum (z | n)) + (Sum <*(z /. (n + 1))*>) by RLVECT_1:41

.= (Sum (z | n)) + (z /. (n + 1)) by RLVECT_1:44 ;

y | n = y | (Seg n) by FINSEQ_1:def 15;

then y = (y | n) ^ <*(y . (n + 1))*> by A4, FINSEQ_3:55;

then y = (y | n) ^ <*(y /. (n + 1))*> by A15, A18;

then A21: Sum y = (Sum (y | n)) + (Sum <*(y /. (n + 1))*>) by RLVECT_1:41

.= (Sum (y | n)) + (y /. (n + 1)) by RLVECT_1:44 ;

x | n = x | (Seg n) by FINSEQ_1:def 15;

then x = (x | n) ^ <*(x . (n + 1))*> by A3, FINSEQ_3:55;

then x = (x | n) ^ <*(x /. (n + 1))*> by A15, A18;

then A22: Sum x = (Sum (x | n)) + (Sum <*(x /. (n + 1))*>) by RLVECT_1:41

.= (Sum (x | n)) + (x /. (n + 1)) by RLVECT_1:44 ;

A23: z /. (n + 1) = z . (n + 1) by A15, A18;

x /. (n + 1) = x . (n + 1) by A15, A18;

then A24: z /. (n + 1) = [(x /. (n + 1)),(y /. (n + 1))] by A6, A19, A23, FINSEQ_1:4;

A25: len (z | n) = n by A5, A7, FINSEQ_1:59;

len (x | n) = n by A3, A7, FINSEQ_1:59;

then Sum (z | n) = [(Sum (x | n)),(Sum (y | n))] by A2, A8, A25, A10;

hence Sum z = [(Sum x),(Sum y)] by A24, A22, A21, A20, Def1; :: thesis: verum

proof

thus
for n being Nat holds S
let x be FinSequence of the carrier of X; :: thesis: for y being FinSequence of the carrier of Y

for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let y be FinSequence of the carrier of Y; :: thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); :: thesis: ( len x = 0 & len y = 0 & len z = 0 & ( for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )

assume that

A27: len x = 0 and

A28: len y = 0 and

A29: len z = 0 and

for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ; :: thesis: Sum z = [(Sum x),(Sum y)]

x = <*> the carrier of X by A27;

then A30: Sum x = 0. X by RLVECT_1:43;

z = <*> the carrier of (Prod_of_RLS (X,Y)) by A29;

then A31: Sum z = 0. (Prod_of_RLS (X,Y)) by RLVECT_1:43;

y = <*> the carrier of Y by A28;

hence Sum z = [(Sum x),(Sum y)] by A30, A31, RLVECT_1:43; :: thesis: verum

end;for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let y be FinSequence of the carrier of Y; :: thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ) holds

Sum z = [(Sum x),(Sum y)]

let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); :: thesis: ( len x = 0 & len y = 0 & len z = 0 & ( for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )

assume that

A27: len x = 0 and

A28: len y = 0 and

A29: len z = 0 and

for i being Nat st i in Seg 0 holds

z . i = [(x . i),(y . i)] ; :: thesis: Sum z = [(Sum x),(Sum y)]

x = <*> the carrier of X by A27;

then A30: Sum x = 0. X by RLVECT_1:43;

z = <*> the carrier of (Prod_of_RLS (X,Y)) by A29;

then A31: Sum z = 0. (Prod_of_RLS (X,Y)) by RLVECT_1:43;

y = <*> the carrier of Y by A28;

hence Sum z = [(Sum x),(Sum y)] by A30, A31, RLVECT_1:43; :: thesis: verum