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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for G being FinSequence of V st len G = k holds
Sum (F ^ G) = (Sum F) + (Sum G) ; :: thesis: S₁[k + 1]
let H be FinSequence of V; :: thesis: ( len H = k + 1 implies Sum (F ^ H) = (Sum F) + (Sum H) )
reconsider p = H | (Seg k) as FinSequence of V by FINSEQ_1:18;
A3: rng H c= the carrier of V by FINSEQ_1:def 4;
assume A4: len H = k + 1 ; :: thesis: Sum (F ^ H) = (Sum F) + (Sum H)
then A5: dom H = Seg (k + 1) by FINSEQ_1:def 3;
then A6: k + 1 in dom H by FINSEQ_1:4;
then H . (k + 1) in rng H by FUNCT_1:def 3;
then reconsider v = H . (k + 1) as Element of V by A3;
A7: k <= k + 1 by NAT_1:12;

A8: now :: thesis: for n being Nat st n in dom p holds
p . n = H . n

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 Seg k by A4, A7, FINSEQ_1:17;
hence p . n = H . n by FUNCT_1:49; :: thesis: verum

end;

A9: dom p = Seg (len p) by FINSEQ_1:def 3;
A10: Seg (len (F ^ p)) = Seg ((len F) + (len p)) by FINSEQ_1:22;
A11: dom (F ^ H) = Seg (len (F ^ H)) by FINSEQ_1:def 3
.= Seg ((len F) + (len H)) by FINSEQ_1:22 ;
A12: dom (F ^ p) = Seg (len (F ^ p)) by FINSEQ_1:def 3;
dom p = Seg k by A4, A7, FINSEQ_1:17;
then A13: dom p c= dom H by A5, A7, FINSEQ_1:5;

A14: now :: thesis: for x being object st x in dom (F ^ p) holds
(F ^ p) . x = (F ^ H) . x

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

A16: now :: thesis: ( not n in dom F implies (F ^ p) . x = (F ^ H) . x )

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

A20: now :: thesis: j <= k

assume not j <= k ; :: thesis: contradiction
then A21: (len F) + k < n by A19, XREAL_1:6;
n <= (len F) + (len p) by A12, A10, A15, FINSEQ_1:1;
hence contradiction by A4, A7, A21, FINSEQ_1:17; :: thesis: verum

end;

now :: thesis: 1 <= j

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

end;

then j in Seg k by A20, FINSEQ_1:1;
then A22: j in dom p by A4, A7, FINSEQ_1:17;
then ( (F ^ p) . n = p . j & (F ^ H) . n = H . j ) by A13, A19, FINSEQ_1:def 7;
hence (F ^ p) . x = (F ^ H) . x by A8, A22; :: thesis: verum

end;

now :: thesis: ( n in dom F implies (F ^ p) . x = (F ^ H) . x )

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

end;

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

end;

A24: len p = k by A4, A7, FINSEQ_1:17;
then (len F) + (len p) <= (len F) + (len H) by A4, A7, XREAL_1:7;
then Seg (len (F ^ p)) c= dom (F ^ H) by A11, A10, FINSEQ_1:5;
then dom (F ^ p) = (dom (F ^ H)) /\ (Seg (len (F ^ p))) by A12, XBOOLE_1:28;
then A25: F ^ p = (F ^ H) | (Seg (len (F ^ p))) by A14, FUNCT_1:46
.= (F ^ H) | (dom (F ^ p)) by FINSEQ_1:def 3 ;

A26: now :: thesis: for n being Nat st n in dom <*v*> holds
H . ((len p) + n) = <*v*> . n

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:2, FINSEQ_1:38;
then n = 1 by TARSKI:def 1;
hence H . ((len p) + n) = <*v*> . n by A24; :: thesis: verum

end;

dom H = Seg ((len p) + (len <*v*>)) by A5, A24, FINSEQ_1:39;
then H = p ^ <*v*> by A8, A26, FINSEQ_1:def 7;
then F ^ H = (F ^ p) ^ <*v*> by FINSEQ_1:32;
then len (F ^ H) = (len (F ^ p)) + (len <*v*>) by FINSEQ_1:22;
then A27: len (F ^ H) = (len (F ^ p)) + 1 by FINSEQ_1:39;
v = (F ^ H) . ((len F) + (len H)) by A4, A6, FINSEQ_1:def 7
.= (F ^ H) . (len (F ^ H)) by FINSEQ_1:22 ;
hence Sum (F ^ H) = (Sum (F ^ p)) + v by A27, A25, Th38
.= ((Sum F) + (Sum p)) + v by A2, A24
.= (Sum F) + ((Sum p) + v) by Def3
.= (Sum F) + (Sum H) by A4, A24, A9, Th38 ;
:: thesis: verum

end;

A28: S₁[ 0 ]

proof

let G be FinSequence 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 ;
then ( F ^ G = F & Sum G = 0. V ) by Lm4, FINSEQ_1:34;
hence Sum (F ^ G) = (Sum F) + (Sum G) by Def4; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A28, A1);
then ( len G = len G implies Sum (F ^ G) = (Sum F) + (Sum G) ) ;
hence Sum (F ^ G) = (Sum F) + (Sum G) ; :: thesis: verum