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 }

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

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 }

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;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;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

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 }

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;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;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

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