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₁[ 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₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

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

proof

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;

A15: for i being Element of NAT st i in Seg (n + 1) holds
( x /. i = x . i & y /. i = y . i & z /. i = z . i )

proof

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;

A18: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A19: y /. (n + 1) = y . (n + 1) by A15;
z | n = z | (Seg n) by FINSEQ_1:def 16;
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 16;
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 16;
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;

end;

A26: S₁[ 0 ]

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

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A26, A1); :: thesis: verum