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

hereby :: thesis: ( RUSp2RNSp X is complete implies 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

proof

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;

hence RUSp2RNSp X is complete by LOPBAN_1:def 15; :: thesis: verum

end;

assume AS2: RUSp2RNSp X is complete ; :: thesis: X is complete
for s1 being sequence of X st s1 is Cauchy holds
s1 is convergent

proof

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;

hence X is complete by BHSP_3:def 4; :: thesis: verum