let V, X be strict RealUnitarySpace; :: thesis: ( V is Subspace of X & X is Subspace of V implies V = X )
assume that
A1: V is Subspace of X and
A2: X is Subspace of V ; :: thesis: V = X
set VX = the carrier of X;
set VV = the carrier of V;
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, A2, Def1;
then A3: the carrier of V = the carrier of X ;
set MX = the Mult of X;
set MV = the Mult of V;
( the Mult of V = the Mult of X | [:REAL, the carrier of V:] & the Mult of X = the Mult of V | [:REAL, the carrier of X:] ) by A1, A2, Def1;
then A4: the Mult of V = the Mult of X by A3, RELAT_1:72;
set AX = the addF of X;
set AV = the addF of V;
( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of V || the carrier of X ) by A1, A2, Def1;
then A5: the addF of V = the addF of X by A3, RELAT_1:72;
set SX = the scalar of X;
set SV = the scalar of V;
A6: the scalar of X = the scalar of V || the carrier of X by A2, Def1;
( 0. V = 0. X & the scalar of V = the scalar of X || the carrier of V ) by A1, Def1;
hence V = X by A3, A5, A4, A6, RELAT_1:72; :: thesis: verum