let M1, M2 be Element of Quot. I; :: thesis: ( ( for z being Element of Q. I holds
( z in M1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) & ( for z being Element of Q. I holds
( z in M2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) implies M1 = M2 )
assume A19: for z being Element of Q. I holds
( z in M1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ; :: thesis: ( ex z being Element of Q. I st
( ( z in M2 implies ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) implies ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) & not z in M2 ) ) or M1 = M2 )
assume A20: for z being Element of Q. I holds
( z in M2 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ; :: thesis: M1 = M2
A21: for x being object st x in M2 holds
x in M1

proof

let x be object ; :: thesis: ( x in M2 implies x in M1 )
assume A22: x in M2 ; :: thesis: x in M1
then reconsider x = x as Element of Q. I ;
ex a, b being Element of Q. I st
( a in u & b in v & (x `1) * ((a `2) * (b `2)) = (x `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) by A20, A22;
hence x in M1 by A19; :: thesis: verum

end;

for x being object st x in M1 holds
x in M2

proof

let x be object ; :: thesis: ( x in M1 implies x in M2 )
assume A23: x in M1 ; :: thesis: x in M2
then reconsider x = x as Element of Q. I ;
ex a, b being Element of Q. I st
( a in u & b in v & (x `1) * ((a `2) * (b `2)) = (x `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) by A19, A23;
hence x in M2 by A20; :: thesis: verum

end;

hence M1 = M2 by A21, TARSKI:2; :: thesis: verum