consider S being strict Submodule of RightModule R such that

A1: the carrier of S = P by Lm10;

reconsider T = RightModStr(# the carrier of S, the addF of S, the ZeroF of S, the rmult of S #) as Submodule of P by A1, Def15;

take T ; :: thesis: T is strict

thus T is strict ; :: thesis: verum

A1: the carrier of S = P by Lm10;

reconsider T = RightModStr(# the carrier of S, the addF of S, the ZeroF of S, the rmult of S #) as Submodule of P by A1, Def15;

take T ; :: thesis: T is strict

thus T is strict ; :: thesis: verum