let a, b be non empty XFinSequence of ; :: thesis: for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & 0 <= b . 0 & b . 0 < m holds
( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )
let m be Nat; :: thesis: ( b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & 0 <= b . 0 & b . 0 < m implies ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) ) )
assume A1: ( b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & 0 <= b . 0 & b . 0 < m ) ; :: thesis: ( ex c being XFinSequence of st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )
then A2: b . 0 in m by NAT_1:45;
A3: 0 < len b by Th2;
reconsider k = b . 0 as Nat by A1;
reconsider Fb = XFS2FS* b as FinSequence of REAL ;
reconsider Fa = XFS2FS* a as FinSequence of REAL ;
reconsider c2 = Fa + Fb as FinSequence of REAL ;
A4: len (XFS2FS* b) = b . 0 by A1, A2, Def4;
A5: len (XFS2FS* a) = b . 0 by A1, A2, Def4;
then A6: len c2 = len (XFS2FS* a) by A4, EUCLID_2:6;
then dom c2 = Seg (len (XFS2FS* b)) by A4, A5, FINSEQ_1:def 3;
then dom ((XFS2FS* a) + (XFS2FS* b)) = dom (XFS2FS* b) by FINSEQ_1:def 3;
then Seg (len c2) = dom (XFS2FS* b) by FINSEQ_1:def 3;
then A7: len c2 = k by A4, FINSEQ_1:def 3;
then consider p being XFinSequence of such that
A8: ( len p = m & p is_an_xrep_of c2 ) by A1, Th7;
set p2 = Replace p,0 ,(b . 0 );
A9: len p = len (Replace p,0 ,(b . 0 )) by AFINSQ_1:48;
ex n being Integer st
( (Replace p,0 ,(b . 0 )) . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
(Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) ) )
proof
A10: ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
(Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) )
proof
now
assume k <> 0 ; :: thesis: for i being Nat st 1 <= i & i <= k holds
(Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i)
thus for i being Nat st 1 <= i & i <= k holds
(Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) :: thesis: verum
proof
let i be Nat; :: thesis: ( 1 <= i & i <= k implies (Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) )
A11: i in NAT by ORDINAL1:def 13;
assume A12: ( 1 <= i & i <= k ) ; :: thesis: (Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i)
then A13: p . i = c2 . i by A7, A8, Def5;
i in Seg (len c2) by A5, A6, A12, FINSEQ_1:3;
then A14: i in dom c2 by FINSEQ_1:def 3;
A15: (XFS2FS* a) . i = a . i by A1, A2, A12, Def4;
(XFS2FS* b) . i = b . i by A1, A2, A12, Def4;
then ((XFS2FS* a) + (XFS2FS* b)) . i = (a . i) + (b . i) by A14, A15, VALUED_1:def 1;
hence (Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) by A11, A12, A13, AFINSQ_1:48; :: thesis: verum
end;
end;
hence ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds
(Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) ) ; :: thesis: verum
end;
(Replace p,0 ,(b . 0 )) . 0 = b . 0 by A1, A8, AFINSQ_1:48;
hence ex n being Integer st
( (Replace p,0 ,(b . 0 )) . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
(Replace p,0 ,(b . 0 )) . i = (a . i) + (b . i) ) ) by A10; :: thesis: verum
end;
then m vector_add_prg Replace p,0 ,(b . 0 ),a,b by A1, A8, A9, Def10;
hence ex c being XFinSequence of st m vector_add_prg c,a,b ; :: thesis: for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
thus for c being non empty XFinSequence of st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) :: thesis: verum
proof
let c be non empty XFinSequence of ; :: thesis: ( m vector_add_prg c,a,b implies XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) )
assume A16: m vector_add_prg c,a,b ; :: thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
then A17: ( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) ) ) by Def10;
consider n being Integer such that
A18: ( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) ) by A16, Def10;
A19: len (XFS2FS* c) = c . 0 by A2, A17, Def4;
now
per cases ( n = 0 or n <> 0 ) ;
case n <> 0 ; :: thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
set p3 = XFS2FS* c;
for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds
(XFS2FS* c) . k3 = c2 . k3
proof
let k3 be Nat; :: thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 )
assume A22: ( 1 <= k3 & k3 <= len (XFS2FS* c) ) ; :: thesis: (XFS2FS* c) . k3 = c2 . k3
A23: c . 0 in len c by A1, A17, NAT_1:45;
then A24: ( len (XFS2FS* c) = n & ( for i being Nat st 1 <= i & i <= n holds
(XFS2FS* c) . i = c . i ) ) by A18, Def4;
A25: ( 1 <= k3 & k3 <= n ) by A18, A22, A23, Def4;
A26: (XFS2FS* c) . k3 = c . k3 by A22, A24
.= (a . k3) + (b . k3) by A18, A25 ;
k3 in Seg (len c2) by A7, A18, A25, FINSEQ_1:3;
then A27: k3 in dom c2 by FINSEQ_1:def 3;
A28: a . k3 = (XFS2FS* a) . k3 by A1, A2, A18, A25, Def4;
b . k3 = (XFS2FS* b) . k3 by A1, A2, A18, A25, Def4;
hence (XFS2FS* c) . k3 = c2 . k3 by A26, A27, A28, VALUED_1:def 1; :: thesis: verum
end;
hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by A7, A18, A19, FINSEQ_1:18; :: thesis: verum
end;
end;
end;
hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ; :: thesis: verum
end;