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;
assume A1: q1. I = q0. I ; :: thesis: contradiction
t `1 = 0. I ;
then t in q0. I by Def8;
then t `1 = t `2 by A1, Def9;
hence contradiction ; :: thesis: verum