let V, X, Y be RealUnitarySpace; :: thesis: ( V is Subspace of X & X is Subspace of Y implies V is Subspace of Y )
assume that
A1: V is Subspace of X and
A2: X is Subspace of Y ; :: thesis: V is Subspace of Y
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y ) by A1, A2, Def1;
hence the carrier of V c= the carrier of Y ; :: according to RUSUB_1:def 1 :: thesis: ( 0. V = 0. Y & the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
0. V = 0. X by A1, Def1;
hence 0. V = 0. Y by A2, Def1; :: thesis: ( the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
thus the addF of V = the addF of Y || the carrier of V :: thesis: ( the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )

proof

set AY = the addF of Y;
set VX = the carrier of X;
set AX = the addF of X;
set VV = the carrier of V;
set AV = the addF of V;
the carrier of V c= the carrier of X by A1, Def1;
then A3: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;
the addF of V = the addF of X || the carrier of V by A1, Def1;
then the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def1;
hence the addF of V = the addF of Y || the carrier of V by A3, FUNCT_1:51; :: thesis: verum

end;

thus the Mult of V = the Mult of Y | [:REAL, the carrier of V:] :: thesis: the scalar of V = the scalar of Y || the carrier of V

proof

set MY = the Mult of Y;
set VX = the carrier of X;
set MX = the Mult of X;
set VV = the carrier of V;
set MV = the Mult of V;
the carrier of V c= the carrier of X by A1, Def1;
then A4: [:REAL, the carrier of V:] c= [:REAL, the carrier of X:] by ZFMISC_1:95;
the Mult of V = the Mult of X | [:REAL, the carrier of V:] by A1, Def1;
then the Mult of V = ( the Mult of Y | [:REAL, the carrier of X:]) | [:REAL, the carrier of V:] by A2, Def1;
hence the Mult of V = the Mult of Y | [:REAL, the carrier of V:] by A4, FUNCT_1:51; :: thesis: verum

end;

set SY = the scalar of Y;
set SX = the scalar of X;
set SV = the scalar of V;
set VX = the carrier of X;
set VV = the carrier of V;
the carrier of V c= the carrier of X by A1, Def1;
then A5: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;
the scalar of V = the scalar of X || the carrier of V by A1, Def1;
then the scalar of V = ( the scalar of Y || the carrier of X) || the carrier of V by A2, Def1;
hence the scalar of V = the scalar of Y || the carrier of V by A5, FUNCT_1:51; :: thesis: verum