let X be RealUnitarySpace; :: thesis: ( X is complete iff RUSp2RNSp X is complete )

set Y = RUSp2RNSp X;

for s1 being sequence of X st s1 is Cauchy holds

s1 is convergent

set Y = RUSp2RNSp X;

hereby :: thesis: ( RUSp2RNSp X is complete implies X is complete )

assume AS2:
RUSp2RNSp X is complete
; :: thesis: X is complete assume AS1:
X is complete
; :: thesis: RUSp2RNSp X is complete

for s2 being sequence of (RUSp2RNSp X) st s2 is Cauchy_sequence_by_Norm holds

s2 is convergent

end;for s2 being sequence of (RUSp2RNSp X) st s2 is Cauchy_sequence_by_Norm holds

s2 is convergent

proof

hence
RUSp2RNSp X is complete
by LOPBAN_1:def 15; :: thesis: verum
let s2 be sequence of (RUSp2RNSp X); :: thesis: ( s2 is Cauchy_sequence_by_Norm implies s2 is convergent )

reconsider s1 = s2 as sequence of X ;

assume s2 is Cauchy_sequence_by_Norm ; :: thesis: s2 is convergent

then s1 is Cauchy by RHS11a;

then s1 is convergent by AS1, BHSP_3:def 4;

hence s2 is convergent by RHS8; :: thesis: verum

end;reconsider s1 = s2 as sequence of X ;

assume s2 is Cauchy_sequence_by_Norm ; :: thesis: s2 is convergent

then s1 is Cauchy by RHS11a;

then s1 is convergent by AS1, BHSP_3:def 4;

hence s2 is convergent by RHS8; :: thesis: verum

for s1 being sequence of X st s1 is Cauchy holds

s1 is convergent

proof

hence
X is complete
by BHSP_3:def 4; :: thesis: verum
let s1 be sequence of X; :: thesis: ( s1 is Cauchy implies s1 is convergent )

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

assume s1 is Cauchy ; :: thesis: s1 is convergent

then s2 is Cauchy_sequence_by_Norm by RHS11a;

then s2 is convergent by AS2, LOPBAN_1:def 15;

hence s1 is convergent by RHS8; :: thesis: verum

end;reconsider s2 = s1 as sequence of (RUSp2RNSp X) ;

assume s1 is Cauchy ; :: thesis: s1 is convergent

then s2 is Cauchy_sequence_by_Norm by RHS11a;

then s2 is convergent by AS2, LOPBAN_1:def 15;

hence s1 is convergent by RHS8; :: thesis: verum