let f1, f2 be Function of (X *),(Y *); :: thesis: ( ( for p being Element of X * holds f1 . p = f * p ) & ( for p being Element of X * holds f2 . p = f * p ) implies f1 = f2 )
assume that
A2: for p being Element of X * holds f1 . p = f * p and
A3: for p being Element of X * holds f2 . p = f * p ; :: thesis: f1 = f2

now :: thesis: for x being Element of X * holds f1 . x = f2 . x

let x be Element of X * ; :: thesis: f1 . x = f2 . x
thus f1 . x = f * x by A2
.= f2 . x by A3 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum