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 and
A2: v in w ; :: thesis: (u `1 ) * (v `2 ) = (v `1 ) * (u `2 )
consider z being Element of Q. I such that
A3: w = QClass. z by Def5;
A4: (u `1 ) * (z `2 ) = (z `1 ) * (u `2 ) by A1, A3, Def4;
z `2 divides z `2 ;
then A5: z `2 divides ((v `2 ) * (u `1 )) * (z `2 ) by GCD_1:7;
A6: (v `1 ) * (z `2 ) = (z `1 ) * (v `2 ) by A2, A3, Def4;
then A7: z `2 divides (z `1 ) * (v `2 ) by GCD_1:def 1;
then A8: z `2 divides ((z `1 ) * (v `2 )) * (u `2 ) by GCD_1:7;
A9: z `2 <> 0. I by Th2;
hence (v `1 ) * (u `2 ) = (((z `1 ) * (v `2 )) / (z `2 )) * (u `2 ) by A6, A7, GCD_1:def 4
.= (((z `1 ) * (v `2 )) * (u `2 )) / (z `2 ) by A7, A8, A9, GCD_1:11
.= ((v `2 ) * ((u `1 ) * (z `2 ))) / (z `2 ) by A4, 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 A5, A9, GCD_1:11
.= ((u `1 ) * (v `2 )) * (1_ I) by A9, GCD_1:9
.= (u `1 ) * (v `2 ) by VECTSP_1:def 13 ;
:: thesis: verum