let z1, z2 be Element of Class (EQRZM V); :: thesis: ( ( for i being Integer st i <> 0 holds

z1 = Class ((EQRZM V),[(0. V),i]) ) & ( for i being Integer st i <> 0 holds

z2 = Class ((EQRZM V),[(0. V),i]) ) implies z1 = z2 )

assume AS1: for i being Integer st i <> 0 holds

z1 = Class ((EQRZM V),[(0. V),i]) ; :: thesis: ( ex i being Integer st

( i <> 0 & not z2 = Class ((EQRZM V),[(0. V),i]) ) or z1 = z2 )

assume AS2: for i being Integer st i <> 0 holds

z2 = Class ((EQRZM V),[(0. V),i]) ; :: thesis: z1 = z2

thus z1 = Class ((EQRZM V),[(0. V),1]) by AS1

.= z2 by AS2 ; :: thesis: verum

z1 = Class ((EQRZM V),[(0. V),i]) ) & ( for i being Integer st i <> 0 holds

z2 = Class ((EQRZM V),[(0. V),i]) ) implies z1 = z2 )

assume AS1: for i being Integer st i <> 0 holds

z1 = Class ((EQRZM V),[(0. V),i]) ; :: thesis: ( ex i being Integer st

( i <> 0 & not z2 = Class ((EQRZM V),[(0. V),i]) ) or z1 = z2 )

assume AS2: for i being Integer st i <> 0 holds

z2 = Class ((EQRZM V),[(0. V),i]) ; :: thesis: z1 = z2

thus z1 = Class ((EQRZM V),[(0. V),1]) by AS1

.= z2 by AS2 ; :: thesis: verum