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
then reconsider res = [a,a] as Element of Q. I by Def1;
A3: for u being object st u in QClass. res holds
u in q1. I

proof

let u be object ; :: thesis: ( u in QClass. res implies u in q1. I )
assume A4: 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)
.= (u `2) * (res `1) by A4, Def4
.= (u `2) * a ;
then u `1 = u `2 by A2, GCD_1:1;
hence u in q1. I by Def9; :: thesis: verum

end;

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

proof

let u be object ; :: thesis: ( u in q1. I implies u in QClass. res )
assume A5: 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
.= (u `2) * a by A5, Def9
.= (u `2) * (res `1) ;
hence u in QClass. res by Def4; :: thesis: verum

end;

then A6: q1. I = QClass. res by A3, TARSKI:2;
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 that
A7: x = QClass. u and
A8: 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 A9: v = [(1. I),a] ; :: thesis: x " = QClass. v
pmult (u,v) = [(a * (v `1)),((u `2) * (v `2))] by A8
.= [(a * (1. I)),((u `2) * (v `2))] by A9
.= [(a * (1. I)),((1. I) * (v `2))] by A8
.= [(a * (1. I)),((1. I) * a)] by A9
.= [a,((1. I) * a)]
.= [a,a] ;
then A10: qmult ((QClass. u),(QClass. v)) = 1. (the_Field_of_Quotients I) by A6, Th10;
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 A7, Def13;
hence x " = QClass. v by A1, A10, VECTSP_1:def 10; :: thesis: verum