let I be non degenerated commutative domRing-like Ring; :: thesis: for x being Element of (the_Field_of_Quotients I) st x <> 0. (the_Field_of_Quotients I) holds
for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let x be Element of (the_Field_of_Quotients I); :: thesis: ( x <> 0. (the_Field_of_Quotients I) implies for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v )
assume A1: x <> 0. (the_Field_of_Quotients I) ; :: thesis: for a being Element of I st a <> 0. I holds
for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let a be Element of I; :: thesis: ( a <> 0. I implies for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v )
assume A2: a <> 0. I ; :: thesis: for u being Element of Q. I st x = QClass. u & u = [a,(1. I)] holds
for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let u be Element of Q. I; :: thesis: ( x = QClass. u & u = [a,(1. I)] implies for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v )
assume A3: ( x = QClass. u & u = [a,(1. I)] ) ; :: thesis: for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let v be Element of Q. I; :: thesis: ( v = [(1. I),a] implies x " = QClass. v )
assume A4: v = [(1. I),a] ; :: thesis: x " = QClass. v
A5: pmult u,v = [(a * (v `1 )),((u `2 ) * (v `2 ))] by A3, MCART_1:def 1
.= [(a * (1. I)),((u `2 ) * (v `2 ))] by A4, MCART_1:def 1
.= [(a * (1. I)),((1. I) * (v `2 ))] by A3, MCART_1:def 2
.= [(a * (1. I)),((1. I) * a)] by A4, MCART_1:def 2
.= [a,((1. I) * a)] by VECTSP_1:def 16
.= [a,a] by VECTSP_1:def 16 ;
reconsider res = [a,a] as Element of Q. I by A2, Def1;
q1. I = QClass. res

proof

A6: for u being set st u in q1. I holds
u in QClass. res

proof

let u be set ; :: thesis: ( u in q1. I implies u in QClass. res )
assume A7: u in q1. I ; :: thesis: u in QClass. res
then reconsider u = u as Element of Q. I ;
(u `1 ) * (res `2 ) = (u `1 ) * a by MCART_1:def 2
.= (u `2 ) * a by A7, Def9
.= (u `2 ) * (res `1 ) by MCART_1:def 1 ;
hence u in QClass. res by Def4; :: thesis: verum

end;

for u being set st u in QClass. res holds
u in q1. I

proof

let u be set ; :: thesis: ( u in QClass. res implies u in q1. I )
assume A8: u in QClass. res ; :: thesis: u in q1. I
then reconsider u = u as Element of Q. I ;
(u `1 ) * a = (u `1 ) * (res `2 ) by MCART_1:def 2
.= (u `2 ) * (res `1 ) by A8, Def4
.= (u `2 ) * a by MCART_1:def 1 ;
then u `1 = u `2 by A2, GCD_1:1;
hence u in q1. I by Def9; :: thesis: verum

end;

hence q1. I = QClass. res by A6, TARSKI:2; :: thesis: verum

end;

then A9: qmult (QClass. u),(QClass. v) = 1. (the_Field_of_Quotients I) by A5, Th12;
reconsider y = QClass. v as Element of (the_Field_of_Quotients I) ;
reconsider y = y as Element of (the_Field_of_Quotients I) ;
qmult (QClass. u),(QClass. v) = x * y by A3, Def13;
hence x " = QClass. v by A1, A9, VECTSP_1:def 22; :: thesis: verum