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_{1}(x)
and

A2: for x being Element of X holds G . x = H_{1}(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_{1}(x)
by A1

.= G . x by A2 ; :: thesis: verum

assume that

A1: for x being Element of X holds F . x = H

A2: for x being Element of X holds G . x = H

let x be Element of X; :: according to FUNCT_2:def 8 :: thesis: F . x = G . x

thus F . x = H

.= G . x by A2 ; :: thesis: verum