let X be set ; :: thesis: for A being Subset of X

for Si being SigmaField of X

for S being SetSequence of Si st S is constant & the_value_of S = A holds

( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )

let A be Subset of X; :: thesis: for Si being SigmaField of X

for S being SetSequence of Si st S is constant & the_value_of S = A holds

( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is constant & the_value_of S = A holds

( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )

let S be SetSequence of Si; :: thesis: ( S is constant & the_value_of S = A implies ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) )

A1: for B being SetSequence of X st B is constant & the_value_of B = A holds

( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )

then ( lim_inf S = A & lim_sup S = A ) by A1;

hence ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) by KURATO_0:def 5; :: thesis: verum

for Si being SigmaField of X

for S being SetSequence of Si st S is constant & the_value_of S = A holds

( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )

let A be Subset of X; :: thesis: for Si being SigmaField of X

for S being SetSequence of Si st S is constant & the_value_of S = A holds

( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is constant & the_value_of S = A holds

( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )

let S be SetSequence of Si; :: thesis: ( S is constant & the_value_of S = A implies ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) )

A1: for B being SetSequence of X st B is constant & the_value_of B = A holds

( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )

proof

assume
( S is constant & the_value_of S = A )
; :: thesis: ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A )
let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) )

A2: ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ;

assume ( B is constant & the_value_of B = A ) ; :: thesis: ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )

hence ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) by A2, Th58; :: thesis: verum

end;A2: ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ;

assume ( B is constant & the_value_of B = A ) ; :: thesis: ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A )

hence ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) by A2, Th58; :: thesis: verum

then ( lim_inf S = A & lim_sup S = A ) by A1;

hence ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) by KURATO_0:def 5; :: thesis: verum