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