let I be non degenerated commutative domRing-like Ring; :: thesis: q1. I <> q0. I
reconsider t = [(0. I),(1_ I)] as Element of Q. I by Def1;
XX: ( [(0. I),(1_ I)] `1 = 0. I & [(0. I),(1_ I)] `2 = 1_ I ) ;
assume A1: q1. I = q0. I ; :: thesis: contradiction
t `1 = 0. I by XX;
then t in q0. I by Def8;
then t `1 = t `2 by A1, Def9;
hence contradiction by XX; :: thesis: verum