let K be Ring; :: thesis: for V being LeftMod of K holds
( V is trivial iff VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) = (0). V )
let V be LeftMod of K; :: thesis: ( V is trivial iff VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) = (0). V )
reconsider W = VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) as strict Subspace of V by Th3;
reconsider Z = (0). V as Subspace of W by VECTSP_4:50;
set X = the carrier of ((0). V);

A1: now

assume not V is trivial ; :: thesis: W <> (0). V
then consider a being Vector of V such that
A2: a <> 0. V by STRUCT_0:def 19;
not a in {(0. V)} by A2, TARSKI:def 1;
then not a in the carrier of ((0). V) by VECTSP_4:def 3;
hence W <> (0). V ; :: thesis: verum

end;

now

assume W <> Z ; :: thesis: not V is trivial
then consider a being Vector of V such that
A3: not a in Z by VECTSP_4:40;
not a in the carrier of ((0). V) by A3, STRUCT_0:def 5;
then not a in {(0. V)} by VECTSP_4:def 3;
then a <> 0. V by TARSKI:def 1;
hence not V is trivial by STRUCT_0:def 19; :: thesis: verum

end;

hence ( V is trivial iff VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) = (0). V ) by A1; :: thesis: verum