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 3
.= (((v `2) * (u `1)) * (z `2)) / (z `2) by GROUP_1:def 3
.= ((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) ;
:: thesis: verum