let F be non degenerated almost_left_invertible commutative domRing-like Ring; :: thesis: F is_ringisomorph_to the_Field_of_Quotients F
A1: 0. F <> 1. F ;
A2: dom (canHom F) = the carrier of F by FUNCT_2:def 1;
A3: for x being set st x in the carrier of (the_Field_of_Quotients F) holds
x in rng (canHom F)

proof

let x be set ; :: thesis: ( x in the carrier of (the_Field_of_Quotients F) implies x in rng (canHom F) )
assume x in the carrier of (the_Field_of_Quotients F) ; :: thesis: x in rng (canHom F)
then reconsider x = x as Element of Quot. F ;
consider u being Element of Q. F such that
A4: x = QClass. u by Def5;
consider a, b being Element of F such that
A5: u = [a,b] and
A6: b <> 0. F by Def1;
consider z being Element of F such that
A7: z * b = 1. F by A6, VECTSP_1:def 20;
reconsider t = [(a * z),(1. F)] as Element of Q. F by A1, Def1;
A8: for x being set st x in QClass. t holds
x in QClass. u

proof

let x be set ; :: thesis: ( x in QClass. t implies x in QClass. u )
assume A9: x in QClass. t ; :: thesis: x in QClass. u
then reconsider x = x as Element of Q. F ;
x `1 = (x `1 ) * (1. F) by VECTSP_1:def 16
.= (x `1 ) * (t `2 ) by MCART_1:def 2
.= (x `2 ) * (t `1 ) by A9, Def4
.= (x `2 ) * (a * z) by MCART_1:def 1 ;
then (x `1 ) * (u `2 ) = ((x `2 ) * (a * z)) * b by A5, MCART_1:def 2
.= (x `2 ) * ((a * z) * b) by GROUP_1:def 4
.= (x `2 ) * (a * (1. F)) by A7, GROUP_1:def 4
.= (x `2 ) * a by VECTSP_1:def 16
.= (x `2 ) * (u `1 ) by A5, MCART_1:def 1 ;
hence x in QClass. u by Def4; :: thesis: verum

end;

for x being set st x in QClass. u holds
x in QClass. t

proof

let x be set ; :: thesis: ( x in QClass. u implies x in QClass. t )
assume A10: x in QClass. u ; :: thesis: x in QClass. t
then reconsider x = x as Element of Q. F ;
(x `1 ) * (t `2 ) = (x `1 ) * (b * z) by A7, MCART_1:def 2
.= ((x `1 ) * b) * z by GROUP_1:def 4
.= ((x `1 ) * (u `2 )) * z by A5, MCART_1:def 2
.= ((x `2 ) * (u `1 )) * z by A10, Def4
.= ((x `2 ) * a) * z by A5, MCART_1:def 1
.= (x `2 ) * (a * z) by GROUP_1:def 4
.= (x `2 ) * (t `1 ) by MCART_1:def 1 ;
hence x in QClass. t by Def4; :: thesis: verum

end;

then A11: QClass. t = QClass. u by A8, TARSKI:2;
(canHom F) . (a * z) = QClass. (quotient (a * z),(1. F)) by Def28
.= x by A1, A4, A11, Def27 ;
hence x in rng (canHom F) by A2, FUNCT_1:def 5; :: thesis: verum

end;

for x being set st x in rng (canHom F) holds
x in the carrier of (the_Field_of_Quotients F) ;
then A12: rng (canHom F) = the carrier of (the_Field_of_Quotients F) by A3, TARSKI:2;
A13: canHom F is RingMonomorphism by Th60;
then canHom F is RingHomomorphism by Def23;
then canHom F is RingEpimorphism by A12, Def22;
hence F is_ringisomorph_to the_Field_of_Quotients F by A13, Def26; :: thesis: verum