let K be Ring; for V being LeftMod of K holds
( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
let V be LeftMod of K; ( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
set X = the carrier of ((0). V);
reconsider W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) as strict Subspace of V by Th3;
reconsider Z = (0). V as Subspace of W by VECTSP_4:39;
hence
( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
by A1; verum