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 for u being object st u in q1. I holds
u in QClass. res 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