let D be non empty set ; :: thesis: for d being Element of D
for f being FinSequence of PFuncs D,REAL st len f <> 0 holds
( d is_common_for_dom f iff d in dom (Sum f) )
let d be Element of D; :: thesis: for f being FinSequence of PFuncs D,REAL st len f <> 0 holds
( d is_common_for_dom f iff d in dom (Sum f) )
defpred S₁[ Element of NAT ] means for f being FinSequence of PFuncs D,REAL st len f = $1 & len f <> 0 holds
( d is_common_for_dom f iff d in dom (Sum f) );
A1: S₁[ 0 ] ;
A2: 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 A3: S₁[n] ; :: thesis: S₁[n + 1]
let f be FinSequence of PFuncs D,REAL ; :: thesis: ( len f = n + 1 & len f <> 0 implies ( d is_common_for_dom f iff d in dom (Sum f) ) )
assume A4: ( len f = n + 1 & len f <> 0 ) ; :: thesis: ( d is_common_for_dom f iff d in dom (Sum f) )
A5: dom f = Seg (len f) by FINSEQ_1:def 3;

now

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

case A6: n = 0 ; :: thesis: ( ( d is_common_for_dom f implies d in dom (Sum f) ) & ( d in dom (Sum f) implies d is_common_for_dom f ) )

then A7: 1 in dom f by A4, FINSEQ_3:27;
then reconsider G = f . 1 as Element of PFuncs D,REAL by FINSEQ_2:13;
f = <*G*> by A4, A6, FINSEQ_1:57;
then A8: Sum f = G by FINSOP_1:12;
hence ( d is_common_for_dom f implies d in dom (Sum f) ) by A7, Def9; :: thesis: ( d in dom (Sum f) implies d is_common_for_dom f )
assume d in dom (Sum f) ; :: thesis: d is_common_for_dom f
then for F being Element of PFuncs D,REAL
for m being Element of NAT st m in dom f & f . m = F holds
d in dom F by A4, A5, A6, A8, FINSEQ_1:4, TARSKI:def 1;
hence d is_common_for_dom f by Def9; :: thesis: verum

end;

case A9: n <> 0 ; :: thesis: ( ( d is_common_for_dom f implies d in dom (Sum f) ) & ( d in dom (Sum f) implies d is_common_for_dom f ) )

then 0 < n ;
then A10: 0 + 1 <= n by NAT_1:13;
set fn = f | n;
n <= n + 1 by NAT_1:11;
then A11: ( len (f | n) = n & n in dom f ) by A4, A10, FINSEQ_1:80, FINSEQ_3:27;
0 + 1 <= n + 1 by NAT_1:13;
then A12: n + 1 in dom f by A4, FINSEQ_3:27;
then reconsider G = f . (n + 1) as Element of PFuncs D,REAL by FINSEQ_2:13;
f = (f | n) ^ <*G*> by A4, RFINSEQ:20;
then A13: Sum f = (Sum (f | n)) + G by Th23;
thus ( d is_common_for_dom f implies d in dom (Sum f) ) :: thesis: ( d in dom (Sum f) implies d is_common_for_dom f )

proof

assume A14: d is_common_for_dom f ; :: thesis: d in dom (Sum f)
then d is_common_for_dom f | n by A9, Th29;
then A15: d in dom (Sum (f | n)) by A3, A9, A11;
d in dom G by A12, A14, Def9;
then d in (dom (Sum (f | n))) /\ (dom G) by A15, XBOOLE_0:def 4;
hence d in dom (Sum f) by A13, VALUED_1:def 1; :: thesis: verum

end;

assume d in dom (Sum f) ; :: thesis: d is_common_for_dom f
then A16: d in (dom (Sum (f | n))) /\ (dom G) by A13, VALUED_1:def 1;
then ( d in dom (Sum (f | n)) & d in dom G ) by XBOOLE_0:def 4;
then A17: d is_common_for_dom f | n by A3, A9, A11;

now

let F be Element of PFuncs D,REAL ; :: thesis: for m being Element of NAT st m in dom f & f . m = F holds
d in dom F
let m be Element of NAT ; :: thesis: ( m in dom f & f . m = F implies d in dom F )
assume A18: ( m in dom f & f . m = F ) ; :: thesis: d in dom F
then A19: ( 1 <= m & m <= len f ) by FINSEQ_3:27;

now

per cases ( m = len f or m <> len f ) ;

case m = len f ; :: thesis: d in dom F

hence d in dom F by A4, A16, A18, XBOOLE_0:def 4; :: thesis: verum

end;

case m <> len f ; :: thesis: d in dom F

then m < len f by A19, XXREAL_0:1;
then m <= n by A4, NAT_1:13;
then A20: ( m in Seg n & dom (f | n) = Seg (len (f | n)) ) by A19, FINSEQ_1:3, FINSEQ_1:def 3;
then F = (f | n) . m by A11, A18, RFINSEQ:19;
hence d in dom F by A11, A17, A20, Def9; :: thesis: verum

end;

end;

end;

hence d in dom F ; :: thesis: verum

end;

hence d is_common_for_dom f by Def9; :: thesis: verum

end;

end;

end;

hence ( d is_common_for_dom f iff d in dom (Sum f) ) ; :: thesis: verum

end;

A21: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
let f be FinSequence of PFuncs D,REAL ; :: thesis: ( len f <> 0 implies ( d is_common_for_dom f iff d in dom (Sum f) ) )
assume len f <> 0 ; :: thesis: ( d is_common_for_dom f iff d in dom (Sum f) )
hence ( d is_common_for_dom f iff d in dom (Sum f) ) by A21; :: thesis: verum