let F, G be Function of X,T; :: thesis: ( ( for x being Element of X holds F . x = (f . x) * (g . x) ) & ( for x being Element of X holds G . x = (f . x) * (g . x) ) implies F = G )
assume that
A1: for x being Element of X holds F . x = H₁(x) and
A2: for x being Element of X holds G . x = H₁(x) ; :: thesis: F = G
let x be Element of X; :: according to FUNCT_2:def 8 :: thesis: F . x = G . x
thus F . x = H₁(x) by A1
.= G . x by A2 ; :: thesis: verum