reconsider V = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) as Z_Module by ZMODUL01:164;
reconsider p = 2 as Element of INT.Ring by INT_1:def 2;
take V ; :: thesis: ex p being Element of INT.Ring st
( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial )
take p ; :: thesis: ( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial )
thus p <> 0. INT.Ring ; :: thesis: not VectQuot (V,(p (*) V)) is trivial
thus not VectQuot (V,(p (*) V)) is trivial :: thesis: verum

proof

reconsider i = 1. INT.Ring as Vector of V ;
i + (p (*) V) is Coset of p (*) V by VECTSP_4:def 6;
then i + (p (*) V) in CosetSet (V,(p (*) V)) ;
then reconsider B = i + (p (*) V) as Element of CosetSet (V,(p (*) V)) ;
reconsider u = B as Vector of (VectQuot (V,(p (*) V))) by VECTSP10:def 6;
u <> 0. (VectQuot (V,(p (*) V)))

proof

assume u = 0. (VectQuot (V,(p (*) V))) ; :: thesis: contradiction
then i + (p (*) V) = zeroCoset (V,(p (*) V)) by VECTSP10:def 6
.= the carrier of (p (*) V) ;
then i in p (*) V by ZMODUL01:63;
then consider w being Vector of V such that
P1: i = p * w ;
reconsider w0 = w as Element of INT.Ring ;
p * w = p * w0 by ZMODUL06:14;
then 1 / 2 = w0 by P1;
hence contradiction by NAT_D:33; :: thesis: verum

end;

hence not VectQuot (V,(p (*) V)) is trivial ; :: thesis: verum

end;