let x1, y1, x2, y2 be G_INTEG; :: thesis: for u1, u2 being Element of Q. Gauss_INT_Ring st y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2 = [x2,y2] holds
( x1 / y1 = x2 / y2 iff QClass. u1 = QClass. u2 )
let u1, u2 be Element of Q. Gauss_INT_Ring; :: thesis: ( y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2 = [x2,y2] implies ( x1 / y1 = x2 / y2 iff QClass. u1 = QClass. u2 ) )
assume A1: ( y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2 = [x2,y2] ) ; :: thesis: ( x1 / y1 = x2 / y2 iff QClass. u1 = QClass. u2 )
A2: (u1 `1) * (u2 `2) = x1 * y2 by Th6, A1;
A3: (u2 `1) * (u1 `2) = x2 * y1 by Th6, A1;
A4: ( (u1 `1) * (u2 `2) = (u2 `1) * (u1 `2) iff u1 in QClass. u2 ) by QUOFIELD:def 4;
( QClass. u1 = QClass. u2 iff u1 in QClass. u2 )

proof

A5: u1 in QClass. u1 by QUOFIELD:5;
thus ( QClass. u1 = QClass. u2 implies u1 in QClass. u2 ) by QUOFIELD:5; :: thesis: ( u1 in QClass. u2 implies QClass. u1 = QClass. u2 )
assume u1 in QClass. u2 ; :: thesis: QClass. u1 = QClass. u2
then u1 in (QClass. u1) /\ (QClass. u2) by A5, XBOOLE_0:def 4;
hence QClass. u1 = QClass. u2 by QUOFIELD:8, XBOOLE_0:def 7; :: thesis: verum

end;

hence ( x1 / y1 = x2 / y2 iff QClass. u1 = QClass. u2 ) by A1, A2, A3, A4, XCMPLX_1:94, XCMPLX_1:95; :: thesis: verum