let V, X, Y be ComplexLinearSpace; ( 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
; 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, Def8;
hence
the carrier of V c= the carrier of Y
; CLVECT_1:def 8 ( 0. V = 0. Y & the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:] )
0. V = 0. X
by A1, Def8;
hence
0. V = 0. Y
by A2, Def8; ( the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:] )
thus
the addF of V = the addF of Y || the carrier of V
the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:]
set MY = the Mult of Y;
set MX = the Mult of X;
set MV = the Mult 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, Def8;
then A4:
[:COMPLEX, the carrier of V:] c= [:COMPLEX, the carrier of X:]
by ZFMISC_1:95;
the Mult of V = the Mult of X | [:COMPLEX, the carrier of V:]
by A1, Def8;
then
the Mult of V = ( the Mult of Y | [:COMPLEX, the carrier of X:]) | [:COMPLEX, the carrier of V:]
by A2, Def8;
hence
the Mult of V = the Mult of Y | [:COMPLEX, the carrier of V:]
by A4, FUNCT_1:51; verum