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 & 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 & 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 that
A1: b . 0 is Nat and
A2: len a = m and
A3: len b = m and
A4: a . 0 = b . 0 and
A5: 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) ) )
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 ;
A6: b . 0 in m by A1, A5, NAT_1:45;
then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def 12;
A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def 12;
then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:145;
then dom c2 = Seg (len (XFS2FS* b)) by A8, A7, 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 A10: len c2 = k by A8, FINSEQ_1:def 3;
then consider p being XFinSequence of such that
A11: len p = m and
A12: p is_an_xrep_of c2 by A5, Th7;
reconsider p2 = Replace p,0 ,(b . 0 ) as XFinSequence of ;
A13: now
assume k <> 0 ; :: thesis: for i being Nat st 1 <= i & i <= k holds
p2 . i = (a . i) + (b . i)
thus for i being Nat st 1 <= i & i <= k holds
p2 . i = (a . i) + (b . i) :: thesis: verum
proof
let i be Nat; :: thesis: ( 1 <= i & i <= k implies p2 . i = (a . i) + (b . i) )
assume that
A14: 1 <= i and
A15: i <= k ; :: thesis: p2 . i = (a . i) + (b . i)
i in Seg (len c2) by A7, A9, A14, A15, FINSEQ_1:3;
then A16: i in dom c2 by FINSEQ_1:def 3;
( (XFS2FS* a) . i = a . i & (XFS2FS* b) . i = b . i ) by A2, A3, A4, A6, A14, A15, AFINSQ_1:def 12;
then A17: ((XFS2FS* a) + (XFS2FS* b)) . i = (a . i) + (b . i) by A16, VALUED_1:def 1;
( i in NAT & p . i = c2 . i ) by A10, A12, A14, A15, Def5, ORDINAL1:def 13;
hence p2 . i = (a . i) + (b . i) by A14, A17, AFINSQ_1:48; :: thesis: verum
end;
end;
( len p = len p2 & p2 . 0 = b . 0 ) by A1, A5, A11, AFINSQ_1:48;
then m vector_add_prg p2,a,b by A2, A3, A11, A13, 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)
A18: 0 < len 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 A19: m vector_add_prg c,a,b ; :: thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
then consider n being Integer such that
A21: c . 0 = b . 0 and
A22: n = b . 0 and
A23: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) by Def10;
A24: ( len c = 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 A19, Def10;
then A25: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def 12;
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 that
A26: 1 <= k3 and
A27: k3 <= len (XFS2FS* c) ; :: thesis: (XFS2FS* c) . k3 = c2 . k3
A28: c . 0 in len c by A1, A5, A24, NAT_1:45;
then A29: k3 <= n by A21, A22, A27, AFINSQ_1:def 12;
then A30: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A22, A26, AFINSQ_1:def 12;
k3 in Seg (len c2) by A10, A22, A26, A29, FINSEQ_1:3;
then A31: k3 in dom c2 by FINSEQ_1:def 3;
len (XFS2FS* c) = n by A21, A22, A28, AFINSQ_1:def 12;
then (XFS2FS* c) . k3 = c . k3 by A21, A22, A26, A27, A28, AFINSQ_1:def 12
.= (a . k3) + (b . k3) by A23, A26, A29 ;
hence (XFS2FS* c) . k3 = c2 . k3 by A31, A30, VALUED_1:def 1; :: thesis: verum
end;
hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by A10, A21, A25, FINSEQ_1:18; :: thesis: verum
end;
end;
end;
hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ; :: thesis: verum
end;