let D be non empty set ; :: thesis: for d being Element of D
for f being FinSequence of PFuncs (D,REAL) st d is_common_for_dom f holds
(Sum f) . d = Sum (f # d)
let d be Element of D; :: thesis: for f being FinSequence of PFuncs (D,REAL) st d is_common_for_dom f holds
(Sum f) . d = Sum (f # d)
defpred S₁[ Nat] means for f being FinSequence of PFuncs (D,REAL) st len f = $1 & d is_common_for_dom f holds
(Sum f) . d = Sum (f # d);
let f be FinSequence of PFuncs (D,REAL); :: thesis: ( d is_common_for_dom f implies (Sum f) . d = Sum (f # d) )
assume A1: d is_common_for_dom f ; :: thesis: (Sum f) . d = Sum (f # d)
A2: len f = len f ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let f be FinSequence of PFuncs (D,REAL); :: thesis: ( len f = n + 1 & d is_common_for_dom f implies (Sum f) . d = Sum (f # d) )
assume that
A5: len f = n + 1 and
A6: d is_common_for_dom f ; :: thesis: (Sum f) . d = Sum (f # d)
set fn = f | n;
A7: len (f | n) = n by A5, FINSEQ_1:59, NAT_1:11;
0 + 1 <= n + 1 by NAT_1:13;
then A8: n + 1 in dom f by A5, FINSEQ_3:25;
then reconsider G = f . (n + 1) as Element of PFuncs (D,REAL) by FINSEQ_2:11;
A9: ( dom f = Seg (len f) & dom (f # d) = Seg (len (f # d)) ) by FINSEQ_1:def 3;
f = (f | n) ^ <*G*> by A5, RFINSEQ:7;
then A10: Sum f = (Sum (f | n)) + G by Th20;
A11: len (f # d) = len f by Def8;
A12: d in dom G by A6, A8;

now :: thesis: ( ( n = 0 & (Sum f) . d = Sum (f # d) ) or ( n <> 0 & (Sum f) . d = Sum (f # d) ) )

per cases ( n = 0 or n <> 0 ) ;

case A13: n = 0 ; :: thesis: (Sum f) . d = Sum (f # d)

then A14: len (f # d) = 1 by A5, Def8;
then A15: 1 in dom (f # d) by FINSEQ_3:25;

A16: now :: thesis: for m being Nat st m in Seg 1 holds
(f # d) . m = <*(G . d)*> . m

let m be Nat; :: thesis: ( m in Seg 1 implies (f # d) . m = <*(G . d)*> . m )
assume m in Seg 1 ; :: thesis: (f # d) . m = <*(G . d)*> . m
then A17: m = 1 by FINSEQ_1:2, TARSKI:def 1;
hence (f # d) . m = G . d by A13, A15, Def8
.= <*(G . d)*> . m by A17 ;
:: thesis: verum

end;

( len <*(G . d)*> = 1 & dom (f # d) = Seg 1 ) by A14, FINSEQ_1:40, FINSEQ_1:def 3;
then A18: f # d = <*(G . d)*> by A14, A16, FINSEQ_2:9;
A19: G . d in REAL by XREAL_0:def 1;
f = <*G*> by A5, A13, FINSEQ_1:40;
hence (Sum f) . d = G . d by FINSOP_1:11
.= Sum (f # d) by A18, A19, FINSOP_1:11 ;
:: thesis: verum

end;

case A20: n <> 0 ; :: thesis: (Sum f) . d = Sum (f # d)

A21: (f # d) . (n + 1) = G . d by A9, A11, A8, Def8;
d is_common_for_dom f | n by A6, A20, Th26;
then d in dom (Sum (f | n)) by A7, A20, Th28;
then d in (dom (Sum (f | n))) /\ (dom G) by A12, XBOOLE_0:def 4;
then d in dom ((Sum (f | n)) + G) by VALUED_1:def 1;
hence (Sum f) . d = ((Sum (f | n)) . d) + (G . d) by A10, VALUED_1:def 1
.= (Sum ((f | n) # d)) + (G . d) by A4, A6, A7, A20, Th26
.= (Sum ((f # d) | n)) + (G . d) by Th29
.= Sum (((f # d) | n) ^ <*(G . d)*>) by RVSUM_1:74
.= Sum (f # d) by A5, A11, A21, RFINSEQ:7 ;
:: thesis: verum

end;

end;

end;

hence (Sum f) . d = Sum (f # d) ; :: thesis: verum

end;

A22: S₁[ 0 ]

proof

let f be FinSequence of PFuncs (D,REAL); :: thesis: ( len f = 0 & d is_common_for_dom f implies (Sum f) . d = Sum (f # d) )
assume that
A23: len f = 0 and
d is_common_for_dom f ; :: thesis: (Sum f) . d = Sum (f # d)
f = <*> (PFuncs (D,REAL)) by A23;
then A24: (Sum f) . d = (([#] D) --> 0) . d by Th19
.= 0 by FUNCOP_1:7 ;
len (f # d) = 0 by A23, Def8;
then f # d = <*> (PFuncs (D,REAL)) ;
hence (Sum f) . d = Sum (f # d) by A24, RVSUM_1:72; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A22, A3);
hence (Sum f) . d = Sum (f # d) by A1, A2; :: thesis: verum