let a, b be non empty XFinSequence of REAL ; :: 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 REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL 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 REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL 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 REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL 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 Segm m by A1, A5, NAT_1:44;

then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def 11;

A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def 11;

then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:115;

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 REAL such that

A11: len p = m and

A12: p is_an_xrep_of c2 by A5, Th2, NUMBERS:19;

reconsider b0 = b . 0 as Element of REAL by XREAL_0:def 1;

reconsider p2 = Replace (p,0,b0) as XFinSequence of REAL ;

then m vector_add_prg p2,a,b by A2, A3, A11, A13;

hence ex c being XFinSequence of REAL st m vector_add_prg c,a,b ; :: thesis: for c being non empty XFinSequence of REAL 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 REAL st m vector_add_prg c,a,b holds

XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) :: thesis: verum

( ex c being XFinSequence of REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL 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 REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL 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 REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL 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 Segm m by A1, A5, NAT_1:44;

then A7: len (XFS2FS* a) = b . 0 by A2, A4, AFINSQ_1:def 11;

A8: len (XFS2FS* b) = b . 0 by A3, A6, AFINSQ_1:def 11;

then A9: len c2 = len (XFS2FS* a) by A7, RVSUM_1:115;

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 REAL such that

A11: len p = m and

A12: p is_an_xrep_of c2 by A5, Th2, NUMBERS:19;

reconsider b0 = b . 0 as Element of REAL by XREAL_0:def 1;

reconsider p2 = Replace (p,0,b0) as XFinSequence of REAL ;

A13: now :: thesis: ( k <> 0 implies for i being Nat st 1 <= i & i <= k holds

p2 . i = (a . i) + (b . i) )

( len p = len p2 & p2 . 0 = b . 0 )
by A1, A5, A11, AFINSQ_1:44;p2 . i = (a . i) + (b . i) )

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

end;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:1;

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

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, ORDINAL1:def 12;

hence p2 . i = (a . i) + (b . i) by A14, A17, AFINSQ_1:44; :: thesis: verum

end;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:1;

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

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, ORDINAL1:def 12;

hence p2 . i = (a . i) + (b . i) by A14, A17, AFINSQ_1:44; :: thesis: verum

then m vector_add_prg p2,a,b by A2, A3, A11, A13;

hence ex c being XFinSequence of REAL st m vector_add_prg c,a,b ; :: thesis: for c being non empty XFinSequence of REAL 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 REAL 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 REAL ; :: 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

A20: c . 0 = b . 0 and

A21: n = b . 0 and

A22: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds

c . i = (a . i) + (b . i) ) ;

A23: ( 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;

then A24: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def 11;

end;assume A19: m vector_add_prg c,a,b ; :: thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)

then consider n being Integer such that

A20: c . 0 = b . 0 and

A21: n = b . 0 and

A22: ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds

c . i = (a . i) + (b . i) ) ;

A23: ( 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;

then A24: len (XFS2FS* c) = c . 0 by A6, AFINSQ_1:def 11;

now :: thesis: ( ( n = 0 & XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) or ( n <> 0 & XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )end;

hence
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

end;

case
n = 0
; :: thesis: XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)

then
( XFS2FS* b = <*> REAL & XFS2FS* c = <*> REAL )
by A18, A23, A21, AFINSQ_1:64;

hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by RVSUM_1:12; :: thesis: verum

end;hence XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) by RVSUM_1:12; :: thesis: verum

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

end;for k3 being Nat st 1 <= k3 & k3 <= len (XFS2FS* c) holds

(XFS2FS* c) . k3 = c2 . k3

proof

hence
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b)
by A10, A20, A24, FINSEQ_1:14; :: thesis: verum
let k3 be Nat; :: thesis: ( 1 <= k3 & k3 <= len (XFS2FS* c) implies (XFS2FS* c) . k3 = c2 . k3 )

assume that

A25: 1 <= k3 and

A26: k3 <= len (XFS2FS* c) ; :: thesis: (XFS2FS* c) . k3 = c2 . k3

A27: c . 0 in len c by A1, A5, A23, AFINSQ_1:86;

then A28: k3 <= n by A20, A21, A26, AFINSQ_1:def 11, A1;

then A29: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A21, A25, AFINSQ_1:def 11;

k3 in Seg (len c2) by A10, A21, A25, A28, FINSEQ_1:1;

then A30: k3 in dom c2 by FINSEQ_1:def 3;

len (XFS2FS* c) = n by A20, A21, A27, AFINSQ_1:def 11, A1;

then (XFS2FS* c) . k3 = c . k3 by A20, A21, A25, A26, A27, AFINSQ_1:def 11

.= (a . k3) + (b . k3) by A22, A25, A28 ;

hence (XFS2FS* c) . k3 = c2 . k3 by A30, A29, VALUED_1:def 1; :: thesis: verum

end;assume that

A25: 1 <= k3 and

A26: k3 <= len (XFS2FS* c) ; :: thesis: (XFS2FS* c) . k3 = c2 . k3

A27: c . 0 in len c by A1, A5, A23, AFINSQ_1:86;

then A28: k3 <= n by A20, A21, A26, AFINSQ_1:def 11, A1;

then A29: ( a . k3 = (XFS2FS* a) . k3 & b . k3 = (XFS2FS* b) . k3 ) by A2, A3, A4, A6, A21, A25, AFINSQ_1:def 11;

k3 in Seg (len c2) by A10, A21, A25, A28, FINSEQ_1:1;

then A30: k3 in dom c2 by FINSEQ_1:def 3;

len (XFS2FS* c) = n by A20, A21, A27, AFINSQ_1:def 11, A1;

then (XFS2FS* c) . k3 = c . k3 by A20, A21, A25, A26, A27, AFINSQ_1:def 11

.= (a . k3) + (b . k3) by A22, A25, A28 ;

hence (XFS2FS* c) . k3 = c2 . k3 by A30, A29, VALUED_1:def 1; :: thesis: verum