let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for X, V being non empty right_complementable strict VectSp-like Abelian add-associative right_zeroed VectSpStr of GF st V is Subspace of X & X is Subspace of V holds
V = X
let X, V be non empty right_complementable strict VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: ( V is Subspace of X & X is Subspace of V implies V = X )
assume A1: ( V is Subspace of X & X is Subspace of V ) ; :: thesis: V = X
set VV = the carrier of V;
set VX = the carrier of X;
set AV = the addF of V;
set AX = the addF of X;
set MV = the lmult of V;
set MX = the lmult of X;
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of V ) by A1, Def2;
then A2: the carrier of V = the carrier of X by XBOOLE_0:def 10;
A3: 0. V = 0. X by A1, Def2;
( 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, Def2;
then A4: the addF of V = the addF of X by A2, RELAT_1:101;
( the lmult of V = the lmult of X | [:the carrier of GF,the carrier of V:] & the lmult of X = the lmult of V | [:the carrier of GF,the carrier of X:] ) by A1, Def2;
hence V = X by A2, A3, A4, RELAT_1:101; :: thesis: verum