let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I st u <> q0. I holds
( qmult u,(qmultinv u) = q1. I & qmult (qmultinv u),u = q1. I )
let u be Element of Quot. I; :: thesis: ( u <> q0. I implies ( qmult u,(qmultinv u) = q1. I & qmult (qmultinv u),u = q1. I ) )
assume A1: u <> q0. I ; :: thesis: ( qmult u,(qmultinv u) = q1. I & qmult (qmultinv u),u = q1. I )
consider x being Element of Q. I such that
A2: qmultinv u = QClass. x by Def5;
consider y being Element of Q. I such that
A3: u = QClass. y by Def5;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then A4: (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;
x in qmultinv u by A2, Th6;
then consider a being Element of Q. I such that
A5: a in u and
A6: (x `1 ) * (a `1 ) = (x `2 ) * (a `2 ) by A1, Def11;
y in u by A3, Th6;
then A7: (y `1 ) * (a `2 ) = (a `1 ) * (y `2 ) by A5, Th8;
A8: a `1 <> 0. I

proof

assume a `1 = 0. I ; :: thesis: contradiction
then a in q0. I by Def8;
then a in (q0. I) /\ u by A5, XBOOLE_0:def 4;
then q0. I meets u by XBOOLE_0:4;
hence contradiction by A1, Th9; :: thesis: verum

end;

A9: a `2 <> 0. I by Th2;
A10: for z being Element of Q. I st z in q1. I holds
z in QClass. t

proof

let z be Element of Q. I; :: thesis: ( z in q1. I implies z in QClass. t )
assume z in q1. I ; :: thesis: z in QClass. t
then z `1 = z `2 by Def9;
then A11: ((z `1 ) * (t `2 )) * ((a `1 ) * (a `2 )) = ((z `2 ) * ((x `2 ) * (y `2 ))) * ((a `1 ) * (a `2 )) by MCART_1:def 2
.= (z `2 ) * (((x `2 ) * (y `2 )) * ((a `1 ) * (a `2 ))) by GROUP_1:def 4
.= (z `2 ) * ((x `2 ) * ((y `2 ) * ((a `1 ) * (a `2 )))) by GROUP_1:def 4
.= (z `2 ) * ((x `2 ) * (((y `1 ) * (a `2 )) * (a `2 ))) by A7, GROUP_1:def 4
.= (z `2 ) * (((x `1 ) * (a `1 )) * ((y `1 ) * (a `2 ))) by A6, GROUP_1:def 4
.= (z `2 ) * ((x `1 ) * ((a `1 ) * ((y `1 ) * (a `2 )))) by GROUP_1:def 4
.= (z `2 ) * ((x `1 ) * ((y `1 ) * ((a `1 ) * (a `2 )))) by GROUP_1:def 4
.= (z `2 ) * (((x `1 ) * (y `1 )) * ((a `1 ) * (a `2 ))) by GROUP_1:def 4
.= ((z `2 ) * ((x `1 ) * (y `1 ))) * ((a `1 ) * (a `2 )) by GROUP_1:def 4
.= ((z `2 ) * (t `1 )) * ((a `1 ) * (a `2 )) by MCART_1:def 1 ;
(a `1 ) * (a `2 ) <> 0. I by A8, A9, VECTSP_2:def 5;
then (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by A11, GCD_1:1;
hence z in QClass. t by Def4; :: thesis: verum

end;

A12: for z being Element of Q. I st z in QClass. t holds
z in q1. I

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies z in q1. I )
assume z in QClass. t ; :: thesis: z in q1. I
then A13: (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by Def4;
(a `2 ) * (a `1 ) <> 0. I by A8, A9, VECTSP_2:def 5;
then A14: ((x `2 ) * (y `2 )) * ((a `2 ) * (a `1 )) <> 0. I by A4, VECTSP_2:def 5;
(z `1 ) * (((x `2 ) * (y `2 )) * ((a `1 ) * (a `2 ))) = ((z `1 ) * ((x `2 ) * (y `2 ))) * ((a `1 ) * (a `2 )) by GROUP_1:def 4
.= ((z `2 ) * (t `1 )) * ((a `1 ) * (a `2 )) by A13, MCART_1:def 2
.= ((z `2 ) * ((x `1 ) * (y `1 ))) * ((a `1 ) * (a `2 )) by MCART_1:def 1
.= (z `2 ) * (((x `1 ) * (y `1 )) * ((a `1 ) * (a `2 ))) by GROUP_1:def 4
.= (z `2 ) * ((((y `1 ) * (x `1 )) * (a `1 )) * (a `2 )) by GROUP_1:def 4
.= (z `2 ) * (((y `1 ) * ((x `2 ) * (a `2 ))) * (a `2 )) by A6, GROUP_1:def 4
.= (z `2 ) * (((x `2 ) * (a `2 )) * ((a `1 ) * (y `2 ))) by A7, GROUP_1:def 4
.= (z `2 ) * ((x `2 ) * ((a `2 ) * ((a `1 ) * (y `2 )))) by GROUP_1:def 4
.= (z `2 ) * ((x `2 ) * ((y `2 ) * ((a `2 ) * (a `1 )))) by GROUP_1:def 4
.= (z `2 ) * (((x `2 ) * (y `2 )) * ((a `2 ) * (a `1 ))) by GROUP_1:def 4 ;
then z `1 = z `2 by A14, GCD_1:1;
hence z in q1. I by Def9; :: thesis: verum

end;

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