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])

z = Class ((EQRZM V),[(0. V),i]) ; :: thesis: verum

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

hence
for i being Integer st i <> 0 holds
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;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

z = Class ((EQRZM V),[(0. V),i]) ; :: thesis: verum