set f = { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ;
A1: for u being set st u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } holds
ex a, b being set st u = [a,b]

proof

let u be set ; :: thesis: ( u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } implies ex a, b being set st u = [a,b] )
assume u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ; :: thesis: ex a, b being set st u = [a,b]
then ex a, b being Element of I st
( u = [a,(QClass. (quotient (a,b)))] & b = 1. I ) ;
hence ex a, b being set st u = [a,b] ; :: thesis: verum

end;

for a, b1, b2 being set st [a,b1] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } & [a,b2] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } holds
b1 = b2

proof

let a, b1, b2 be set ; :: thesis: ( [a,b1] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } & [a,b2] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } implies b1 = b2 )
assume that
A2: [a,b1] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } and
A3: [a,b2] in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ; :: thesis: b1 = b2
consider x1, x2 being Element of I such that
A4: [a,b1] = [x1,(QClass. (quotient (x1,x2)))] and
A5: x2 = 1. I by A2;
A6: a = [x1,(QClass. (quotient (x1,x2)))] `1 by A4, MCART_1:def 1
.= x1 by MCART_1:def 1 ;
consider y1, y2 being Element of I such that
A7: [a,b2] = [y1,(QClass. (quotient (y1,y2)))] and
A8: y2 = 1. I by A3;
A9: a = [y1,(QClass. (quotient (y1,y2)))] `1 by A7, MCART_1:def 1
.= y1 by MCART_1:def 1 ;
reconsider a = a as Element of I by A6;
b1 = [a,b2] `2 by A4, A5, A7, A8, A6, A9, MCART_1:def 2
.= b2 by MCART_1:def 2 ;
hence b1 = b2 ; :: thesis: verum

end;

then reconsider f = { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;
A10: for x being set st x in dom f holds
x in the carrier of I

proof

let x be set ; :: thesis: ( x in dom f implies x in the carrier of I )
assume x in dom f ; :: thesis: x in the carrier of I
then consider y being set such that
A11: [x,y] in f by RELAT_1:def 4;
consider a, b being Element of I such that
A12: [x,y] = [a,(QClass. (quotient (a,b)))] and
b = 1. I by A11;
x = [a,(QClass. (quotient (a,b)))] `1 by A12, MCART_1:def 1
.= a by MCART_1:def 1 ;
hence x in the carrier of I ; :: thesis: verum

end;

for x being set st x in the carrier of I holds
x in dom f

proof

let x be set ; :: thesis: ( x in the carrier of I implies x in dom f )
assume x in the carrier of I ; :: thesis: x in dom f
then reconsider x = x as Element of I ;
[x,(QClass. (quotient (x,(1. I))))] in f ;
hence x in dom f by RELAT_1:def 4; :: thesis: verum

end;

then A13: dom f = the carrier of I by A10, TARSKI:2;
for y being set st y in rng f holds
y in the carrier of (the_Field_of_Quotients I)

proof

let y be set ; :: thesis: ( y in rng f implies y in the carrier of (the_Field_of_Quotients I) )
assume y in rng f ; :: thesis: y in the carrier of (the_Field_of_Quotients I)
then consider x being set such that
A14: [x,y] in f by RELAT_1:def 5;
consider a, b being Element of I such that
A15: [x,y] = [a,(QClass. (quotient (a,b)))] and
b = 1. I by A14;
y = [a,(QClass. (quotient (a,b)))] `2 by A15, MCART_1:def 2
.= QClass. (quotient (a,b)) by MCART_1:def 2 ;
hence y in the carrier of (the_Field_of_Quotients I) ; :: thesis: verum

end;

then rng f c= the carrier of (the_Field_of_Quotients I) by TARSKI:def 3;
then reconsider f = f as Function of I,(the_Field_of_Quotients I) by A13, FUNCT_2:def 1, RELSET_1:11;
for x being Element of I holds f . x = QClass. (quotient (x,(1. I)))

proof

let x be Element of I; :: thesis: f . x = QClass. (quotient (x,(1. I)))
[x,(QClass. (quotient (x,(1. I))))] in f ;
hence f . x = QClass. (quotient (x,(1. I))) by A13, FUNCT_1:def 4; :: thesis: verum

end;

hence ex b₁ being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b₁ . x = QClass. (quotient (x,(1. I))) ; :: thesis: verum