let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of Q. I st ex w being Element of Quot. I st
( u in w & v in w ) holds
(u `1 ) * (v `2 ) = (v `1 ) * (u `2 )
let u, v be Element of Q. I; :: thesis: ( ex w being Element of Quot. I st
( u in w & v in w ) implies (u `1 ) * (v `2 ) = (v `1 ) * (u `2 ) )
given w being Element of Quot. I such that A1: ( u in w & v in w ) ; :: thesis: (u `1 ) * (v `2 ) = (v `1 ) * (u `2 )
consider z being Element of Q. I such that
A2: w = QClass. z by Def5;
A3: (u `1 ) * (z `2 ) = (z `1 ) * (u `2 ) by A1, A2, Def4;
A4: (v `1 ) * (z `2 ) = (z `1 ) * (v `2 ) by A1, A2, Def4;
then A5: z `2 divides (z `1 ) * (v `2 ) by GCD_1:def 1;
then A6: z `2 divides ((z `1 ) * (v `2 )) * (u `2 ) by GCD_1:7;
z `2 divides z `2 ;
then A7: z `2 divides ((v `2 ) * (u `1 )) * (z `2 ) by GCD_1:7;
A8: z `2 <> 0. I by Th2;
hence (v `1 ) * (u `2 ) = (((z `1 ) * (v `2 )) / (z `2 )) * (u `2 ) by A4, A5, GCD_1:def 4
.= (((z `1 ) * (v `2 )) * (u `2 )) / (z `2 ) by A5, A6, A8, GCD_1:11
.= ((v `2 ) * ((u `1 ) * (z `2 ))) / (z `2 ) by A3, GROUP_1:def 4
.= (((v `2 ) * (u `1 )) * (z `2 )) / (z `2 ) by GROUP_1:def 4
.= ((v `2 ) * (u `1 )) * ((z `2 ) / (z `2 )) by A7, A8, GCD_1:11
.= ((u `1 ) * (v `2 )) * (1_ I) by A8, GCD_1:9
.= (u `1 ) * (v `2 ) by VECTSP_1:def 13 ;
:: thesis: verum