let R be Ring; 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; ( 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
; 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:]
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; verum