1_ I <> 0. I ;
then reconsider t = [(1_ I),(1_ I)] as Element of Q. I by Def1;
set M = QClass. t;
A1: for z being Element of Q. I st z in QClass. t holds
z `1 = z `2

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies z `1 = z `2 )
assume z in QClass. t ; :: thesis: z `1 = z `2
then A2: (z `1) * (t `2) = (z `2) * (t `1) by Def4;
z `1 = (z `1) * (1_ I)
.= (z `2) * (t `1) by A2
.= (z `2) * (1_ I)
.= z `2 ;
hence z `1 = z `2 ; :: thesis: verum

end;

for z being Element of Q. I st z `1 = z `2 holds
z in QClass. t

proof

let z be Element of Q. I; :: thesis: ( z `1 = z `2 implies z in QClass. t )
assume z `1 = z `2 ; :: thesis: z in QClass. t
then (z `1) * (t `2) = (z `2) * (1_ I)
.= (z `2) * (t `1) ;
hence z in QClass. t by Def4; :: thesis: verum

end;

hence ex b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff z `1 = z `2 ) by A1; :: thesis: verum