theorem :: EQREL_1:56

for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G