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₁[ Element of 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 Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of 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:80, NAT_1:11;
0 + 1 <= n + 1 by NAT_1:13;
then A8: n + 1 in dom f by A5, FINSEQ_3:27;
then reconsider G = f . (n + 1) as Element of PFuncs D,REAL by FINSEQ_2:13;
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:20;
then A10: Sum f = (Sum (f | n)) + G by Th23;
A11: len (f # d) = len f by Def8;
A12: d in dom G by A6, A8, Def9;

now

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:27;

A16: now

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:4, TARSKI:def 1;
hence (f # d) . m = G . d by A13, A15, Def8
.= <*(G . d)*> . m by A17, FINSEQ_1:57 ;
:: thesis: verum

end;

( len <*(G . d)*> = 1 & dom (f # d) = Seg 1 ) by A14, FINSEQ_1:57, FINSEQ_1:def 3;
then A18: f # d = <*(G . d)*> by A14, A16, FINSEQ_2:10;
f = <*G*> by A5, A13, FINSEQ_1:57;
hence (Sum f) . d = G . d by FINSOP_1:12
.= Sum (f # d) by A18, FINSOP_1:12 ;
:: thesis: verum

end;

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

A20: (f # d) . (n + 1) = G . d by A9, A11, A8, Def8;
d is_common_for_dom f | n by A6, A19, Th29;
then d in dom (Sum (f | n)) by A7, A19, Th31;
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, A19, Th29
.= (Sum ((f # d) | n)) + (G . d) by Th32
.= Sum (((f # d) | n) ^ <*(G . d)*>) by RVSUM_1:104
.= Sum (f # d) by A5, A11, A20, RFINSEQ:20 ;
:: thesis: verum

end;

end;

end;

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

end;

A21: 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
A22: len f = 0 and
d is_common_for_dom f ; :: thesis: (Sum f) . d = Sum (f # d)
f = <*> (PFuncs D,REAL ) by A22;
then A23: (Sum f) . d = (([#] D) --> 0 ) . d by Th21
.= 0 by FUNCOP_1:13 ;
len (f # d) = 0 by A22, Def8;
then f # d = <*> (PFuncs D,REAL ) ;
hence (Sum f) . d = Sum (f # d) by A23, RVSUM_1:102; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A21, A3);
hence (Sum f) . d = Sum (f # d) by A1, A2; :: thesis: verum