let X, Y be set ; :: thesis: for f1, f2 being Function of X,Y st ( for x being object st x in X holds
f1 . x = f2 . x ) holds
f1 = f2
let f1, f2 be Function of X,Y; :: thesis: ( ( for x being object st x in X holds
f1 . x = f2 . x ) implies f1 = f2 )

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: ( ( for x being object st x in X holds
f1 . x = f2 . x ) implies f1 = f2 )

hence ( ( for x being object st x in X holds
f1 . x = f2 . x ) implies f1 = f2 ) ; :: thesis: verum

end;

suppose Y <> {} ; :: thesis: ( ( for x being object st x in X holds
f1 . x = f2 . x ) implies f1 = f2 )

then ( dom f1 = X & dom f2 = X ) by Def1;
hence ( ( for x being object st x in X holds
f1 . x = f2 . x ) implies f1 = f2 ) ; :: thesis: verum

end;

end;