let X be set ; :: thesis: for y being object
for f1, f2 being Function of X,{y} holds f1 = f2
let y be object ; :: 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 object st x in X holds
f1 . x = f2 . x

proof

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

end;

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