let X, y be set ; :: thesis: for f1, f2 being Function of X,{y} holds f1 = f2
let f1, f2 be Function of X,{y}; :: thesis: f1 = f2
for x being set st x in X holds
f1 . x = f2 . x

proof

let x be set ; :: thesis: ( x in X implies f1 . x = f2 . x )
assume A1: x in X ; :: thesis: f1 . x = f2 . x
then f1 . x = y by Th65;
hence f1 . x = f2 . x by A1, Th65; :: thesis: verum

end;

hence f1 = f2 by Th18; :: thesis: verum