set f = { [x,(QClass. (quotient x,y))] where x, y is Element of I : y = 1. I } ;
A1: { [x,(QClass. (quotient x,y))] where x, y is Element of I : y = 1. I } is Relation-like

proof

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;

hence { [x,(QClass. (quotient x,y))] where x, y is Element of I : y = 1. I } is Relation-like by RELAT_1:def 1; :: thesis: verum

end;

{ [x,(QClass. (quotient x,y))] where x, y is Element of I : y = 1. I } is Function-like

proof

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 A2: ( [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 } ) ; :: thesis: b1 = b2
then consider x1, x2 being Element of I such that
A3: ( [a,b1] = [x1,(QClass. (quotient x1,x2))] & x2 = 1. I ) ;
consider y1, y2 being Element of I such that
A4: ( [a,b2] = [y1,(QClass. (quotient y1,y2))] & y2 = 1. I ) by A2;
A5: a = [x1,(QClass. (quotient x1,x2))] `1 by A3, MCART_1:def 1
.= x1 by MCART_1:def 1 ;
A6: a = [y1,(QClass. (quotient y1,y2))] `1 by A4, MCART_1:def 1
.= y1 by MCART_1:def 1 ;
reconsider a = a as Element of I by A5;
b1 = [a,b2] `2 by A3, A4, A5, A6, MCART_1:def 2
.= b2 by MCART_1:def 2 ;
hence b1 = b2 ; :: thesis: verum

end;

hence { [x,(QClass. (quotient x,y))] where x, y is Element of I : y = 1. I } is Function-like by FUNCT_1:def 1; :: 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;
A7: dom f = the carrier of I

proof

A8: 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
A9: [x,y] in f by RELAT_1:def 4;
consider a, b being Element of I such that
A10: ( [x,y] = [a,(QClass. (quotient a,b))] & b = 1. I ) by A9;
x = [a,(QClass. (quotient a,b))] `1 by A10, 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;

hence dom f = the carrier of I by A8, TARSKI:2; :: thesis: verum

end;

rng f c= the carrier of (the_Field_of_Quotients I)

proof

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
A11: [x,y] in f by RELAT_1:def 5;
consider a, b being Element of I such that
A12: ( [x,y] = [a,(QClass. (quotient a,b))] & b = 1. I ) by A11;
y = [a,(QClass. (quotient a,b))] `2 by A12, 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;

hence rng f c= the carrier of (the_Field_of_Quotients I) by TARSKI:def 3; :: thesis: verum

end;

then reconsider f = f as Function of I,(the_Field_of_Quotients I) by A7, 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 A7, 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