set f = { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } ;
A1: for u being object st u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } holds
ex a, b being object st u = [a,b]
proof
let u be object ; :: thesis: ( u in { [x,(QClass. (quotient (x,y)))] where x, y is Element of I : y = 1. I } implies ex a, b being object 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 object 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 object st u = [a,b] ; :: thesis: verum
end;
for a, b1, b2 being object 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 object ; :: 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 by A4, XTUPLE_0: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 by A7, XTUPLE_0:1;
reconsider a = a as Element of I by A6;
b1 = b2 by A4, A5, A7, A8, A6, A9, XTUPLE_0:1;
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 object st x in dom f holds
x in the carrier of I
proof
let x be object ; :: 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 object such that
A11: [x,y] in f by XTUPLE_0:def 12;
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 by A12, XTUPLE_0:1;
hence x in the carrier of I ; :: thesis: verum
end;
for x being object st x in the carrier of I holds
x in dom f
proof
let x be object ; :: 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 XTUPLE_0:def 12; :: thesis: verum
end;
then A13: dom f = the carrier of I by A10, TARSKI:2;
for y being object st y in rng f holds
y in the carrier of (the_Field_of_Quotients I)
proof
let y be object ; :: 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 object such that
A14: [x,y] in f by XTUPLE_0:def 13;
consider a, b being Element of I such that
A15: [x,y] = [a,(QClass. (quotient (a,b)))] and
b = 1. I by A14;
y = QClass. (quotient (a,b)) by A15, XTUPLE_0:1;
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:4;
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 2; :: thesis: verum
end;
hence ex b1 being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b1 . x = QClass. (quotient (x,(1. I))) ; :: thesis: verum