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)
.= 0. I ;
thus z `1 = 0. I by A2; :: 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
.= (z `2) * (0. I)
.= (z `2) * (t `1) ;
hence z in QClass. t by Def4; :: thesis: verum
end;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I ) by A1; :: thesis: verum