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