let X, Y be RealNormSpace; :: thesis: ( ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism implies ( X is complete iff Y is complete ) )
given L being Lipschitzian LinearOperator of X,Y such that A1: L is isomorphism ; :: thesis: ( X is complete iff Y is complete )

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

assume A2: X is complete ; :: thesis: Y is complete
for seq being sequence of Y st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof

let seq be sequence of Y; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume A3: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
consider K being Lipschitzian LinearOperator of Y,X such that
A4: ( K = L " & K is isomorphism ) by A1, NISOM01;
K * seq is Cauchy_sequence_by_Norm by A3, A4, NISOM05;
then K * seq is convergent by A2, LOPBAN_1:def 15;
hence seq is convergent by A4, NISOM03; :: thesis: verum

end;

hence Y is complete by LOPBAN_1:def 15; :: thesis: verum

end;

assume A5: Y is complete ; :: thesis: X is complete
for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof

let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
then L * seq is Cauchy_sequence_by_Norm by A1, NISOM05;
then L * seq is convergent by A5, LOPBAN_1:def 15;
hence seq is convergent by A1, NISOM03; :: thesis: verum

end;

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