let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V, X, Y being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y
let V, X, Y be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: ( V is Subspace of X & X is Subspace of Y implies V is Subspace of Y )
assume A1: ( V is Subspace of X & X is Subspace of Y ) ; :: thesis: V is Subspace of Y
A2: the carrier of V c= the carrier of Y

proof

( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y ) by A1, Def2;
hence the carrier of V c= the carrier of Y by XBOOLE_1:1; :: thesis: verum

end;

A3: 0. V = 0. Y

proof

( 0. V = 0. X & 0. X = 0. Y ) by A1, Def2;
hence 0. V = 0. Y ; :: thesis: verum

end;

A4: the addF of V = the addF of Y || the carrier of V

proof

set AV = the addF of V;
set VV = the carrier of V;
set AX = the addF of X;
set VX = the carrier of X;
set AY = the addF of Y;
( the addF of V = the addF of X || the carrier of V & the addF of X = the addF of Y || the carrier of X & the carrier of V c= the carrier of X ) by A1, Def2;
then ( the addF of V = (the addF of Y || the carrier of X) || the carrier of V & [:the carrier of V,the carrier of V:] c= [:the carrier of X,the carrier of X:] ) by ZFMISC_1:119;
hence the addF of V = the addF of Y || the carrier of V by FUNCT_1:82; :: thesis: verum

end;

set MV = the lmult of V;
set VV = the carrier of V;
set MX = the lmult of X;
set VX = the carrier of X;
set MY = the lmult of Y;
( the lmult of V = the lmult of X | [:the carrier of GF,the carrier of V:] & the lmult of X = the lmult of Y | [:the carrier of GF,the carrier of X:] & the carrier of V c= the carrier of X ) by A1, Def2;
then ( the lmult of V = (the lmult of Y | [:the carrier of GF,the carrier of X:]) | [:the carrier of GF,the carrier of V:] & [:the carrier of GF,the carrier of V:] c= [:the carrier of GF,the carrier of X:] ) by ZFMISC_1:118;
then the lmult of V = the lmult of Y | [:the carrier of GF,the carrier of V:] by FUNCT_1:82;
hence V is Subspace of Y by A2, A3, A4, Def2; :: thesis: verum