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) );
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 A1: len f <> 0 ; :: thesis: ( d is_common_for_dom f iff d in dom (Sum f) )
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 that
A4: len f = n + 1 and
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 ) )

A10: n <= n + 1 by NAT_1:11;
0 + 1 <= n by A9, NAT_1:13;
then A11: n in dom f by A4, A10, 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;
set fn = f | n;
A13: len (f | n) = n by A4, FINSEQ_1:80, NAT_1:11;
f = (f | n) ^ <*G*> by A4, RFINSEQ:20;
then A14: 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 A15: d is_common_for_dom f ; :: thesis: d in dom (Sum f)
then d is_common_for_dom f | n by A9, Th29;
then A16: d in dom (Sum (f | n)) by A3, A9, A13;
d in dom G by A12, A15, Def9;
then d in (dom (Sum (f | n))) /\ (dom G) by A16, XBOOLE_0:def 4;
hence d in dom (Sum f) by A14, VALUED_1:def 1; :: thesis: verum

end;

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

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 that
A19: m in dom f and
A20: f . m = F ; :: thesis: d in dom F
A21: m <= len f by A19, FINSEQ_3:27;
A22: 1 <= m by A19, 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, A17, A20, XBOOLE_0:def 4; :: thesis: verum

end;

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

then m < len f by A21, XXREAL_0:1;
then m <= n by A4, NAT_1:13;
then A23: m in Seg n by A22, FINSEQ_1:3;
then ( dom (f | n) = Seg (len (f | n)) & F = (f | n) . m ) by A11, A20, FINSEQ_1:def 3, RFINSEQ:19;
hence d in dom F by A13, A18, A23, 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;

A24: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A24, A2);
hence ( d is_common_for_dom f iff d in dom (Sum f) ) by A1; :: thesis: verum