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 }
A1: dom ((Partial_Sums (Re F)) . n) = meet { (dom ((Re F) . k)) where k is Element of NAT : k <= n } by Lem07;
dom ((Partial_Sums (Re F)) . n) = dom ((Re (Partial_Sums F)) . n) by Lm326;
then A2: dom ((Partial_Sums (Re F)) . n) = dom ((Partial_Sums F) . n) by MESFUN7C:def 11;

now

let A be set ; :: 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
A3: ( A = dom ((Re F) . i) & i <= n ) ;
A = dom (F . i) by A3, MESFUN7C:def 11;
hence A in { (dom (F . k)) where k is Element of NAT : k <= n } by A3; :: thesis: verum

end;

then A4: { (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

let A be set ; :: 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
A5: ( A = dom (F . i) & i <= n ) ;
A = dom ((Re F) . i) by A5, MESFUN7C:def 11;
hence A in { (dom ((Re F) . k)) where k is Element of NAT : k <= n } by A5; :: thesis: verum

end;

then { (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;
hence dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n } by A1, A2, A4, XBOOLE_0:def 10; :: thesis: verum