let X be RealUnitarySpace; :: thesis: for Y being Subset of X holds

( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y )

let Y be Subset of X; :: thesis: ( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y )

lim s in Y ; :: thesis: Y is closed

reconsider Z = Y as Subset of (RUSp2RNSp X) ;

for s1 being sequence of (RUSp2RNSp X) st rng s1 c= Z & s1 is convergent holds

lim s1 in Z

hence Y is closed ; :: thesis: verum

( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y )

let Y be Subset of X; :: thesis: ( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y )

hereby :: thesis: ( ( for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y ) implies Y is closed )

assume A4:
for s being sequence of X st rng s c= Y & s is convergent holds lim s in Y ) implies Y is closed )

assume
Y is closed
; :: thesis: for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y

then consider Z being Subset of (RUSp2RNSp X) such that

A1: ( Z = Y & Z is closed ) ;

thus for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y :: thesis: verum

end;lim s in Y

then consider Z being Subset of (RUSp2RNSp X) such that

A1: ( Z = Y & Z is closed ) ;

thus for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y :: thesis: verum

proof

let s be sequence of X; :: thesis: ( rng s c= Y & s is convergent implies lim s in Y )

assume A3: ( rng s c= Y & s is convergent ) ; :: thesis: lim s in Y

reconsider s1 = s as sequence of (RUSp2RNSp X) ;

( rng s1 c= Z & s1 is convergent ) by A3, A1, RHS8;

then lim s1 in Z by A1;

hence lim s in Y by A1, A3, RHS9; :: thesis: verum

end;assume A3: ( rng s c= Y & s is convergent ) ; :: thesis: lim s in Y

reconsider s1 = s as sequence of (RUSp2RNSp X) ;

( rng s1 c= Z & s1 is convergent ) by A3, A1, RHS8;

then lim s1 in Z by A1;

hence lim s in Y by A1, A3, RHS9; :: thesis: verum

lim s in Y ; :: thesis: Y is closed

reconsider Z = Y as Subset of (RUSp2RNSp X) ;

for s1 being sequence of (RUSp2RNSp X) st rng s1 c= Z & s1 is convergent holds

lim s1 in Z

proof

then
Z is closed
;
let s1 be sequence of (RUSp2RNSp X); :: thesis: ( rng s1 c= Z & s1 is convergent implies lim s1 in Z )

assume A5: ( rng s1 c= Z & s1 is convergent ) ; :: thesis: lim s1 in Z

reconsider s = s1 as sequence of X ;

A6: ( rng s c= Y & s is convergent ) by A5, RHS8;

then lim s in Y by A4;

hence lim s1 in Z by A6, RHS9; :: thesis: verum

end;assume A5: ( rng s1 c= Z & s1 is convergent ) ; :: thesis: lim s1 in Z

reconsider s = s1 as sequence of X ;

A6: ( rng s c= Y & s is convergent ) by A5, RHS8;

then lim s in Y by A4;

hence lim s1 in Z by A6, RHS9; :: thesis: verum

hence Y is closed ; :: thesis: verum