let X be non empty set ; :: thesis: for n being Nat
for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
let n be Nat; :: thesis: for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }
let F be Functional_Sequence of X,COMPLEX; :: thesis: dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }

now :: thesis: for A being object st A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n } holds
A in { (dom (F . k)) where k is Element of NAT : k <= n }

let A be object ; :: thesis: ( A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n } implies A in { (dom (F . k)) where k is Element of NAT : k <= n } )
assume A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n } ; :: thesis: A in { (dom (F . k)) where k is Element of NAT : k <= n }
then consider i being Element of NAT such that
A1: A = dom ((Re F) . i) and
A2: i <= n ;
A = dom (F . i) by A1, MESFUN7C:def 11;
hence A in { (dom (F . k)) where k is Element of NAT : k <= n } by A2; :: thesis: verum

end;

then A3: { (dom ((Re F) . k)) where k is Element of NAT : k <= n } c= { (dom (F . k)) where k is Element of NAT : k <= n } by TARSKI:def 3;

now :: thesis: for A being object st A in { (dom (F . k)) where k is Element of NAT : k <= n } holds
A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n }

let A be object ; :: thesis: ( A in { (dom (F . k)) where k is Element of NAT : k <= n } implies A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n } )
assume A in { (dom (F . k)) where k is Element of NAT : k <= n } ; :: thesis: A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n }
then consider i being Element of NAT such that
A4: A = dom (F . i) and
A5: i <= n ;
A = dom ((Re F) . i) by A4, MESFUN7C:def 11;
hence A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n } by A5; :: thesis: verum

end;

then A6: { (dom (F . k)) where k is Element of NAT : k <= n } c= { (dom ((Re F) . k)) where k is Element of NAT : k <= n } by TARSKI:def 3;
dom ((Partial_Sums (Re F)) . n) = dom ((Re (Partial_Sums F)) . n) by Th29;
then A7: dom ((Partial_Sums (Re F)) . n) = dom ((Partial_Sums F) . n) by MESFUN7C:def 11;
dom ((Partial_Sums (Re F)) . n) = meet { (dom ((Re F) . k)) where k is Element of NAT : k <= n } by Th10;
hence dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } by A7, A3, A6, XBOOLE_0:def 10; :: thesis: verum