X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then 1 in INT \ {0} by XBOOLE_0:def 5, X1;
then [(0. V),1] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;
then reconsider z = Class ((EQRZM V),[(0. V),1]) as Element of Class (EQRZM V) by EQREL_1:def 3;
take z ; :: thesis: for i being Integer st i <> 0 holds
z = Class ((EQRZM V),[(0. V),i])
for i being Integer st i <> 0 holds
z = Class ((EQRZM V),[(0. V),i])

proof

let i be Integer; :: thesis: ( i <> 0 implies z = Class ((EQRZM V),[(0. V),i]) )
assume X2: i <> 0 ; :: thesis: z = Class ((EQRZM V),[(0. V),i])
then X21: not i in {0} by TARSKI:def 1;
Z1: i in INT by INT_1:def 2;
then i in INT \ {0} by XBOOLE_0:def 5, X21;
then X3: [(0. V),i] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;
reconsider i = i as Element of INT.Ring by Z1;
(1. INT.Ring) * (0. V) = 0. V by ZMODUL01:1
.= i * (0. V) by ZMODUL01:1 ;
then [[(0. V),i],[(0. V),1]] in EQRZM V by AS, X2, LMEQR001;
hence z = Class ((EQRZM V),[(0. V),i]) by X3, EQREL_1:35; :: thesis: verum

end;

hence for i being Integer st i <> 0 holds
z = Class ((EQRZM V),[(0. V),i]) ; :: thesis: verum