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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: for G being FinSequence of V st len G = k holds
Sum (F ^ G) = (Sum F) + (Sum G) ; :: thesis: S1[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;
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, FINSEQ_1:def 8; :: 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: S1[ 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 S1[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