let x, A be set ; :: thesis: for f, g being Function of {x},A st f . x = g . x holds
f = g
let f, g be Function of {x},A; :: thesis: ( f . x = g . x implies f = g )
assume A1: f . x = g . x ; :: thesis: f = g

now :: thesis: for y being object st y in {x} holds
f . y = g . y

let y be object ; :: thesis: ( y in {x} implies f . y = g . y )
assume y in {x} ; :: thesis: f . y = g . y
then y = x by TARSKI:def 1;
hence f . y = g . y by A1; :: thesis: verum

end;

hence f = g ; :: thesis: verum