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
; 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;
( i <> 0 implies z = Class ((EQRZM V),[(0. V),i]) )
assume X2:
i <> 0
;
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;
verum
end;
hence
for i being Integer st i <> 0 holds
z = Class ((EQRZM V),[(0. V),i])
; verum