let f1, f2 be Function of R,(Frac S); :: thesis: ( ( for o being object st o in the carrier of R holds
f1 . o = [o,(1. R)] ) & ( for o being object st o in the carrier of R holds
f2 . o = [o,(1. R)] ) implies f1 = f2 )
assume that
A2: for o being object st o in the carrier of R holds
f1 . o = [o,(1. R)] and
A3: for o being object st o in the carrier of R holds
f2 . o = [o,(1. R)] ; :: thesis: f1 = f2
for o1 being object st o1 in the carrier of R holds
f1 . o1 = f2 . o1

proof

let o1 be object ; :: thesis: ( o1 in the carrier of R implies f1 . o1 = f2 . o1 )
assume A4: o1 in the carrier of R ; :: thesis: f1 . o1 = f2 . o1
f1 . o1 = [o1,(1. R)] by A2, A4;
hence f1 . o1 = f2 . o1 by A3, A4; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum