(Omega). V <> (0). V ;
then consider v being Vector of V such that
A1: ( v in (Omega). V & v <> 0. V ) by ZMODUL04:24;
take v ; :: thesis: not v is zero
thus not v is zero by A1; :: thesis: verum