let I be non degenerated commutative domRing-like Ring; 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); ( 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)
; 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; ( 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
; 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; ( 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)]
; for v being Element of Q. I st v = [(1. I),a] holds
x " = QClass. v
let v be Element of Q. I; ( v = [(1. I),a] implies x " = QClass. v )
assume A9:
v = [(1. I),a]
; 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; verum