let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I holds
( qmult u,(q1. I) = u & qmult (q1. I),u = u )
let u be Element of Quot. I; :: thesis: ( qmult u,(q1. I) = u & qmult (q1. I),u = u )
consider x being Element of Q. I such that
A1: q1. I = QClass. x by Def5;
consider y being Element of Q. I such that
A2: u = QClass. y by Def5;
A3: qmult u,(q1. I) = QClass. (pmult y,x) by A1, A2, Th12;
x in q1. I by A1, Th6;
then A4: x `1 = x `2 by Def9;
A5: ( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then (x `2 ) * (y `2 ) <> 0. I by VECTSP_2:def 5;
then reconsider t = [((x `1 ) * (y `1 )),((x `2 ) * (y `2 ))] as Element of Q. I by Def1;
A6: for z being Element of Q. I st z in QClass. y holds
z in QClass. t

proof

let z be Element of Q. I; :: thesis: ( z in QClass. y implies z in QClass. t )
assume z in QClass. y ; :: thesis: z in QClass. t
then A7: (z `1 ) * (y `2 ) = (z `2 ) * (y `1 ) by Def4;
(z `1 ) * (t `2 ) = (z `1 ) * ((x `2 ) * (y `2 )) by MCART_1:def 2
.= ((z `2 ) * (y `1 )) * (x `2 ) by A7, GROUP_1:def 4
.= (z `2 ) * ((x `1 ) * (y `1 )) by A4, GROUP_1:def 4
.= (z `2 ) * (t `1 ) by MCART_1:def 1 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

A8: for z being Element of Q. I st z in QClass. t holds
z in QClass. y

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies z in QClass. y )
assume z in QClass. t ; :: thesis: z in QClass. y
then (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by Def4;
then A9: (z `1 ) * ((x `2 ) * (y `2 )) = (z `2 ) * (t `1 ) by MCART_1:def 2;
A10: ((z `1 ) * (y `2 )) * (x `2 ) = (z `1 ) * ((x `2 ) * (y `2 )) by GROUP_1:def 4
.= (z `2 ) * ((x `2 ) * (y `1 )) by A4, A9, MCART_1:def 1
.= ((z `2 ) * (y `1 )) * (x `2 ) by GROUP_1:def 4 ;
x `2 divides x `2 ;
then A11: x `2 divides ((z `1 ) * (y `2 )) * (x `2 ) by GCD_1:7;
x `2 divides x `2 ;
then A12: x `2 divides ((z `2 ) * (y `1 )) * (x `2 ) by GCD_1:7;
(z `1 ) * (y `2 ) = ((z `1 ) * (y `2 )) * (1_ I) by VECTSP_1:def 13
.= ((z `1 ) * (y `2 )) * ((x `2 ) / (x `2 )) by A5, GCD_1:9
.= (((z `2 ) * (y `1 )) * (x `2 )) / (x `2 ) by A5, A10, A11, GCD_1:11
.= ((z `2 ) * (y `1 )) * ((x `2 ) / (x `2 )) by A5, A12, GCD_1:11
.= ((z `2 ) * (y `1 )) * (1_ I) by A5, GCD_1:9
.= (z `2 ) * (y `1 ) by VECTSP_1:def 13 ;
hence z in QClass. y by Def4; :: thesis: verum

end;

qmult (q1. I),u = QClass. (pmult x,y) by A1, A2, Th12;
hence ( qmult u,(q1. I) = u & qmult (q1. I),u = u ) by A2, A3, A6, A8, SUBSET_1:8; :: thesis: verum