let V be non empty add-associative right_zeroed addLoopStr ; :: thesis: for F, G being FinSequence of the carrier of V holds Sum (F ^ G) = (Sum F) + (Sum G)
let F, G be FinSequence of the carrier of V; :: thesis: Sum (F ^ G) = (Sum F) + (Sum G)
defpred S₁[ set ] means for G being FinSequence of the carrier of V st len G = $1 holds
Sum (F ^ G) = (Sum F) + (Sum G);
A1: S₁[ 0 ]

proof

let G be FinSequence of the carrier of V; :: thesis: ( len G = 0 implies Sum (F ^ G) = (Sum F) + (Sum G) )
assume len G = 0 ; :: thesis: Sum (F ^ G) = (Sum F) + (Sum G)
then ( G = <*> the carrier of V & G = {} ) ;
then ( F ^ G = F & Sum G = 0. V ) by Lm4, FINSEQ_1:47;
hence Sum (F ^ G) = (Sum F) + (Sum G) by Def7; :: thesis: verum

end;

A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: for G being FinSequence of the carrier of V st len G = k holds
Sum (F ^ G) = (Sum F) + (Sum G) ; :: thesis: S₁[k + 1]
let H be FinSequence of the carrier of V; :: thesis: ( len H = k + 1 implies Sum (F ^ H) = (Sum F) + (Sum H) )
assume A4: len H = k + 1 ; :: thesis: Sum (F ^ H) = (Sum F) + (Sum H)
reconsider p = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:23;
A5: dom H = Seg (k + 1) by A4, FINSEQ_1:def 3;
then A6: k + 1 in dom H by FINSEQ_1:6;
then ( H . (k + 1) in rng H & rng H c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider v = H . (k + 1) as Element of V ;
A7: k <= k + 1 by NAT_1:12;
then A8: len p = k by A4, FINSEQ_1:21;
then A9: dom H = Seg ((len p) + (len <*v*>)) by A5, FINSEQ_1:56;
dom p = Seg k by A4, A7, FINSEQ_1:21;
then A10: dom p c= dom H by A5, A7, FINSEQ_1:7;

A11: now

let n be Nat; :: thesis: ( n in dom p implies p . n = H . n )
assume n in dom p ; :: thesis: p . n = H . n
then ( n in dom H & n in Seg k ) by A4, A7, A10, FINSEQ_1:21;
hence p . n = H . n by FUNCT_1:72; :: thesis: verum

end;

now

let n be Nat; :: thesis: ( n in dom <*v*> implies H . ((len p) + n) = <*v*> . n )
assume n in dom <*v*> ; :: thesis: H . ((len p) + n) = <*v*> . n
then n in {1} by FINSEQ_1:4, FINSEQ_1:55;
then n = 1 by TARSKI:def 1;
hence H . ((len p) + n) = <*v*> . n by A8, FINSEQ_1:def 8; :: thesis: verum

end;

then H = p ^ <*v*> by A9, A11, FINSEQ_1:def 7;
then F ^ H = (F ^ p) ^ <*v*> by FINSEQ_1:45;
then len (F ^ H) = (len (F ^ p)) + (len <*v*>) by FINSEQ_1:35;
then A12: len (F ^ H) = (len (F ^ p)) + 1 by FINSEQ_1:56;
A13: dom (F ^ p) = Seg (len (F ^ p)) by FINSEQ_1:def 3;
A14: dom (F ^ H) = Seg (len (F ^ H)) by FINSEQ_1:def 3
.= Seg ((len F) + (len H)) by FINSEQ_1:35 ;
A15: Seg (len (F ^ p)) = Seg ((len F) + (len p)) by FINSEQ_1:35;
(len F) + (len p) <= (len F) + (len H) by A4, A7, A8, XREAL_1:9;
then Seg (len (F ^ p)) c= dom (F ^ H) by A14, A15, FINSEQ_1:7;
then A16: dom (F ^ p) = (dom (F ^ H)) /\ (Seg (len (F ^ p))) by A13, XBOOLE_1:28;

now

let x be set ; :: thesis: ( x in dom (F ^ p) implies (F ^ p) . x = (F ^ H) . x )
assume A17: x in dom (F ^ p) ; :: thesis: (F ^ p) . x = (F ^ H) . x
then reconsider n = x as Element of NAT ;

A18: now

assume n in dom F ; :: thesis: (F ^ p) . x = (F ^ H) . x
then ( (F ^ p) . n = F . n & (F ^ H) . n = F . n ) by FINSEQ_1:def 7;
hence (F ^ p) . x = (F ^ H) . x ; :: thesis: verum

end;

now

assume not n in dom F ; :: thesis: (F ^ p) . x = (F ^ H) . x
then A19: not n in Seg (len F) by FINSEQ_1:def 3;
A20: 1 <= n by A13, A17, FINSEQ_1:3;
then len F <= n by A19, FINSEQ_1:3;
then consider j being Nat such that
A21: n = (len F) + j by NAT_1:10;

A22: now

assume not 1 <= j ; :: thesis: contradiction
then j = 0 by NAT_1:14;
hence contradiction by A19, A20, A21, FINSEQ_1:3; :: thesis: verum

end;

now

assume not j <= k ; :: thesis: contradiction
then ( (len F) + k < n & n <= (len F) + (len p) ) by A13, A15, A17, A21, FINSEQ_1:3, XREAL_1:8;
hence contradiction by A4, A7, FINSEQ_1:21; :: thesis: verum

end;

then j in Seg k by A22, FINSEQ_1:3;
then A23: j in dom p by A4, A7, FINSEQ_1:21;
then ( (F ^ p) . n = p . j & (F ^ H) . n = H . j ) by A10, A21, FINSEQ_1:def 7;
hence (F ^ p) . x = (F ^ H) . x by A11, A23; :: thesis: verum

end;

hence (F ^ p) . x = (F ^ H) . x by A18; :: thesis: verum

end;

then A24: F ^ p = (F ^ H) | (Seg (len (F ^ p))) by A16, FUNCT_1:68, FUNCT_1:70, RELAT_1:90
.= (F ^ H) | (dom (F ^ p)) by FINSEQ_1:def 3 ;
A25: dom p = Seg (len p) by FINSEQ_1:def 3;
v = (F ^ H) . ((len F) + (len H)) by A4, A6, FINSEQ_1:def 7
.= (F ^ H) . (len (F ^ H)) by FINSEQ_1:35 ;
hence Sum (F ^ H) = (Sum (F ^ p)) + v by A12, A24, Th55
.= ((Sum F) + (Sum p)) + v by A3, A8
.= (Sum F) + ((Sum p) + v) by Def6
.= (Sum F) + (Sum H) by A4, A8, A25, Th55 ;
:: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
then ( len G = len G implies Sum (F ^ G) = (Sum F) + (Sum G) ) ;
hence Sum (F ^ G) = (Sum F) + (Sum G) ; :: thesis: verum