theorem :: FUNCT_3:63

for X, Y, Z being set
for f1, f2 being Function of X,Y
for g1, g2 being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) & <:f1,g1:> = <:f2,g2:> holds
( f1 = f2 & g1 = g2 )