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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
thus S1[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 ;
A9: Seg n c= Seg (n + 1) by ;
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 ;
(x | n) . i = x . i by ;
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 ;
hence ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) by ; :: 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 15;
then z = (z | n) ^ <*(z . (n + 1))*> by ;
then z = (z | n) ^ <*(z /. (n + 1))*> by ;
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 ;
then y = (y | n) ^ <*(y /. (n + 1))*> by ;
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 ;
then x = (x | n) ^ <*(x /. (n + 1))*> by ;
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 ;
x /. (n + 1) = x . (n + 1) by ;
then A24: z /. (n + 1) = [(x /. (n + 1)),(y /. (n + 1))] by ;
A25: len (z | n) = n by ;
len (x | n) = n by ;
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: S1[ 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 ; :: thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A26, A1); :: thesis: verum