let f1, f2 be Function of I,(the_Field_of_Quotients I); :: thesis: ( ( for x being Element of I holds f1 . x = QClass. (quotient (x,(1. I))) ) & ( for x being Element of I holds f2 . x = QClass. (quotient (x,(1. I))) ) implies f1 = f2 )
assume A16: for x being Element of I holds f1 . x = QClass. (quotient (x,(1. I))) ; :: thesis: ( ex x being Element of I st not f2 . x = QClass. (quotient (x,(1. I))) or f1 = f2 )
assume A17: for x being Element of I holds f2 . x = QClass. (quotient (x,(1. I))) ; :: thesis: f1 = f2
for x being object st x in the carrier of I holds
f1 . x = f2 . x
proof
let x be object ; :: thesis: ( x in the carrier of I implies f1 . x = f2 . x )
assume x in the carrier of I ; :: thesis: f1 . x = f2 . x
then reconsider x = x as Element of I ;
f1 . x = QClass. (quotient (x,(1. I))) by A16
.= f2 . x by A17 ;
hence f1 . x = f2 . x ; :: thesis: verum
end;
hence f1 = f2 ; :: thesis: verum