reconsider t = [(0. 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 = 0. I

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies z `1 = 0. I )
assume z in QClass. t ; :: thesis: z `1 = 0. I
then A2: (z `1) * (t `2) = (z `2) * (t `1) by Def4
.= (z `2) * (0. I) by MCART_1:def 1
.= 0. I by VECTSP_1:7 ;
t `2 <> 0. I by Th2;
hence z `1 = 0. I by A2, VECTSP_2:def 1; :: thesis: verum

end;

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

proof

let z be Element of Q. I; :: thesis: ( z `1 = 0. I implies z in QClass. t )
assume z `1 = 0. I ; :: thesis: z in QClass. t
then (z `1) * (t `2) = 0. I by VECTSP_1:7
.= (z `2) * (0. I) by VECTSP_1:7
.= (z `2) * (t `1) by MCART_1:def 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 = 0. I ) by A1; :: thesis: verum