let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for X, V being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st V is Subspace of X & X is Subspace of V holds

V = X

let X, V be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: 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, Def2;

then A3: the carrier of V = the carrier of X ;

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, Def2;

then A4: the addF of V = the addF of X by A3;

set MX = the lmult of X;

set MV = the lmult of V;

A5: the lmult of X = the lmult of V | [: the carrier of GF, the carrier of X:] by A2, Def2;

( 0. V = 0. X & the lmult of V = the lmult of X | [: the carrier of GF, the carrier of V:] ) by A1, Def2;

hence V = X by A3, A4, A5; :: thesis: verum

V = X

let X, V be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: 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, Def2;

then A3: the carrier of V = the carrier of X ;

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, Def2;

then A4: the addF of V = the addF of X by A3;

set MX = the lmult of X;

set MV = the lmult of V;

A5: the lmult of X = the lmult of V | [: the carrier of GF, the carrier of X:] by A2, Def2;

( 0. V = 0. X & the lmult of V = the lmult of X | [: the carrier of GF, the carrier of V:] ) by A1, Def2;

hence V = X by A3, A4, A5; :: thesis: verum