let f1, f2 be Function of A,(S ~ A); :: thesis: ( ( for o being object st o in the carrier of A holds
f1 . o = Class ((EqRel S),((frac1 S) . o)) ) & ( for o being object st o in the carrier of A holds
f2 . o = Class ((EqRel S),((frac1 S) . o)) ) implies f1 = f2 )
assume that
A2: for o being object st o in the carrier of A holds
f1 . o = Class ((EqRel S),((frac1 S) . o)) and
A3: for o being object st o in the carrier of A holds
f2 . o = Class ((EqRel S),((frac1 S) . o)) ; :: thesis: f1 = f2
for o1 being object st o1 in the carrier of A holds
f1 . o1 = f2 . o1

proof

let o1 be object ; :: thesis: ( o1 in the carrier of A implies f1 . o1 = f2 . o1 )
assume A4: o1 in the carrier of A ; :: thesis: f1 . o1 = f2 . o1
f1 . o1 = Class ((EqRel S),((frac1 S) . o1)) by A2, A4;
hence f1 . o1 = f2 . o1 by A3, A4; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum