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

proof

let n be 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 :: thesis: ( ( n = 0 & ( d is_common_for_dom f implies d in dom (Sum f) ) & ( d in dom (Sum f) implies d is_common_for_dom f ) ) or ( n <> 0 & ( d is_common_for_dom f implies d in dom (Sum f) ) & ( d in dom (Sum f) implies d is_common_for_dom f ) ) )

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:25;
then reconsider G = f . 1 as Element of PFuncs (D,REAL) by FINSEQ_2:11;
f = <*G*> by A4, A6, FINSEQ_1:40;
then A8: Sum f = G by FINSOP_1:11;
hence ( d is_common_for_dom f implies d in dom (Sum f) ) by A7; :: 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 m being Nat st m in dom f holds
d in dom (f . m) by A4, A5, A6, A8, FINSEQ_1:2, TARSKI:def 1;
hence d is_common_for_dom f ; :: 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:25;
0 + 1 <= n + 1 by NAT_1:13;
then A12: n + 1 in dom f by A4, FINSEQ_3:25;
then reconsider G = f . (n + 1) as Element of PFuncs (D,REAL) by FINSEQ_2:11;
set fn = f | n;
A13: len (f | n) = n by A4, FINSEQ_1:59, NAT_1:11;
f = (f | n) ^ <*G*> by A4, RFINSEQ:7;
then A14: Sum f = (Sum (f | n)) + G by Th20;
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, Th26;
then A16: d in dom (Sum (f | n)) by A3, A9, A13;
d in dom G by A12, A15;
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 :: thesis: for m being Nat st m in dom f holds
d in dom (f . m)

let m be Nat; :: thesis: ( m in dom f implies d in dom (f . m) )
assume A19: m in dom f ; :: thesis: d in dom (f . m)
set F = f . m;
A20: m <= len f by A19, FINSEQ_3:25;
A21: 1 <= m by A19, FINSEQ_3:25;

now :: thesis: ( ( m = len f & d in dom (f . m) ) or ( m <> len f & d in dom (f . m) ) )

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

case m = len f ; :: thesis: d in dom (f . m)

hence d in dom (f . m) by A4, A17, XBOOLE_0:def 4; :: thesis: verum

end;

case m <> len f ; :: thesis: d in dom (f . m)

then m < len f by A20, XXREAL_0:1;
then m <= n by A4, NAT_1:13;
then A22: m in Seg n by A21, FINSEQ_1:1;
then ( dom (f | n) = Seg (len (f | n)) & f . m = (f | n) . m ) by A11, FINSEQ_1:def 3, RFINSEQ:6;
hence d in dom (f . m) by A13, A18, A22; :: thesis: verum

end;

end;

end;

hence d in dom (f . m) ; :: thesis: verum

end;

hence d is_common_for_dom f ; :: thesis: verum

end;

end;

end;

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

end;

A23: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A23, A2);
hence ( d is_common_for_dom f iff d in dom (Sum f) ) by A1; :: thesis: verum