let X, Y be RealLinearSpace; :: thesis: for n being Element of 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 Element of NAT st i in Seg n holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
defpred S₁[ Element of 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 Element of NAT st i in Seg $1 holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)];
A1: 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 Element of 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 Element of 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 Element of NAT st i in Seg 0 holds
z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )
assume that
A2: ( len x = 0 & len y = 0 & len z = 0 ) and
for i being Element of 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 & y = <*> the carrier of Y & z = <*> the carrier of (Prod_of_RLS X,Y) ) by A2;
then ( Sum x = 0. X & Sum y = 0. Y & Sum z = 0. (Prod_of_RLS X,Y) ) by RLVECT_1:60;
hence Sum z = [(Sum x),(Sum y)] ; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: 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 Element of 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 Element of 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 Element of NAT st i in Seg (n + 1) holds
z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )
assume that
A5: ( len x = n + 1 & len y = n + 1 & len z = n + 1 ) and
A6: for i being Element of NAT st i in Seg (n + 1) holds
z . i = [(x . i),(y . i)] ; :: thesis: Sum z = [(Sum x),(Sum y)]
A7: 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 i in Seg (n + 1) ; :: thesis: ( x /. i = x . i & y /. i = y . i & z /. i = z . i )
then ( 1 <= i & i <= n + 1 ) by FINSEQ_1:3;
hence ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) by A5, FINSEQ_4:24; :: thesis: verum

end;

A8: n + 1 in Seg (n + 1) by FINSEQ_1:6;
then ( x /. (n + 1) = x . (n + 1) & y /. (n + 1) = y . (n + 1) & z /. (n + 1) = z . (n + 1) ) by A7;
then A9: z /. (n + 1) = [(x /. (n + 1)),(y /. (n + 1))] by A6, FINSEQ_1:6;
A10: 0 + n <= 1 + n by XREAL_1:8;
then A11: ( len (x | n) = n & len (y | n) = n & len (z | n) = n ) by A5, FINSEQ_1:80;
A12: Seg n c= Seg (n + 1) by A10, FINSEQ_1:7;
for i being Element of NAT st i in Seg n holds
(z | n) . i = [((x | n) . i),((y | n) . i)]

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (z | n) . i = [((x | n) . i),((y | n) . i)] )
assume A13: i in Seg n ; :: thesis: (z | n) . i = [((x | n) . i),((y | n) . i)]
then i <= n by FINSEQ_1:3;
then ( (x | n) . i = x . i & (y | n) . i = y . i & (z | n) . i = z . i ) by FINSEQ_3:121;
hence (z | n) . i = [((x | n) . i),((y | n) . i)] by A6, A12, A13; :: thesis: verum

end;

then A14: Sum (z | n) = [(Sum (x | n)),(Sum (y | n))] by A4, A11;
( len x = n + 1 & x | n = x | (Seg n) ) by A5, FINSEQ_1:def 15;
then x = (x | n) ^ <*(x . (n + 1))*> by FINSEQ_3:61;
then x = (x | n) ^ <*(x /. (n + 1))*> by A7, A8;
then A15: Sum x = (Sum (x | n)) + (Sum <*(x /. (n + 1))*>) by RLVECT_1:58
.= (Sum (x | n)) + (x /. (n + 1)) by RLVECT_1:61 ;
( len y = n + 1 & y | n = y | (Seg n) ) by A5, FINSEQ_1:def 15;
then y = (y | n) ^ <*(y . (n + 1))*> by FINSEQ_3:61;
then y = (y | n) ^ <*(y /. (n + 1))*> by A7, A8;
then A16: Sum y = (Sum (y | n)) + (Sum <*(y /. (n + 1))*>) by RLVECT_1:58
.= (Sum (y | n)) + (y /. (n + 1)) by RLVECT_1:61 ;
( len z = n + 1 & z | n = z | (Seg n) ) by A5, FINSEQ_1:def 15;
then z = (z | n) ^ <*(z . (n + 1))*> by FINSEQ_3:61;
then z = (z | n) ^ <*(z /. (n + 1))*> by A7, A8;
then Sum z = (Sum (z | n)) + (Sum <*(z /. (n + 1))*>) by RLVECT_1:58
.= (Sum (z | n)) + (z /. (n + 1)) by RLVECT_1:61 ;
hence Sum z = [(Sum x),(Sum y)] by A9, A14, A15, A16, Def1; :: thesis: verum

end;

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A3); :: thesis: verum