let R be Ring; :: thesis: for V, X, Y being RightMod of R st V is Submodule of X & X is Submodule of Y holds
V is Submodule of Y
let V, X, Y be RightMod of R; :: thesis: ( V is Submodule of X & X is Submodule of Y implies V is Submodule of Y )
assume that
A1: V is Submodule of X and
A2: X is Submodule of Y ; :: thesis: V is Submodule of Y
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y ) by A1, A2, Def2;
then A3: the carrier of V c= the carrier of Y ;
A4: the addF of V = the addF of Y | [: the carrier of V, 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, Def2;
then A5: [: 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, Def2;
then the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def2;
hence the addF of V = the addF of Y | [: the carrier of V, the carrier of V:] by A5, FUNCT_1:51; :: thesis: verum

end;

set MY = the rmult of Y;
set MX = the rmult of X;
set MV = the rmult 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, Def2;
then A6: [: the carrier of V, the carrier of R:] c= [: the carrier of X, the carrier of R:] by ZFMISC_1:95;
the rmult of V = the rmult of X | [: the carrier of V, the carrier of R:] by A1, Def2;
then the rmult of V = ( the rmult of Y | [: the carrier of X, the carrier of R:]) | [: the carrier of V, the carrier of R:] by A2, Def2;
then A7: the rmult of V = the rmult of Y | [: the carrier of V, the carrier of R:] by A6, FUNCT_1:51;
0. V = 0. X by A1, Def2;
then 0. V = 0. Y by A2, Def2;
hence V is Submodule of Y by A3, A4, A7, Def2; :: thesis: verum