let X, Y be RealNormSpace; :: thesis: ( ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism implies ( X is separable iff Y is separable ) )
given L being Lipschitzian LinearOperator of X,Y such that A1: L is isomorphism ; :: thesis: ( X is separable iff Y is separable )
consider K being Lipschitzian LinearOperator of Y,X such that
A2: ( K = L " & K is isomorphism ) by A1, NORMSP_3:37;
hereby :: thesis: ( Y is separable implies X is separable )
assume X is separable ; :: thesis: Y is separable
then consider seq being sequence of X such that
A3: rng seq is dense by NORMSP_3:21;
reconsider seq1 = L * seq as sequence of Y ;
rng seq1 = L .: (rng seq) by RELAT_1:127;
then rng seq1 is dense by A1, A3, Th30;
hence Y is separable by NORMSP_3:21; :: thesis: verum
end;
assume Y is separable ; :: thesis: X is separable
then consider seq being sequence of Y such that
A4: rng seq is dense by NORMSP_3:21;
reconsider seq1 = K * seq as sequence of X ;
rng seq1 = K .: (rng seq) by RELAT_1:127;
then rng seq1 is dense by A2, A4, Th30;
hence X is separable by NORMSP_3:21; :: thesis: verum