let X, Y be set ; :: thesis: for f1, f2 being Function of X,Y st ( for x being Element of X holds f1 . x = f2 . x ) holds
f1 = f2
let f1, f2 be Function of X,Y; :: thesis: ( ( for x being Element of X holds f1 . x = f2 . x ) implies f1 = f2 )
assume for x being Element of X holds f1 . x = f2 . x ; :: thesis: f1 = f2
then for x being object st x in X holds
f1 . x = f2 . x ;
hence f1 = f2 by Th12; :: thesis: verum