theorem :: FUNCT_3:78

for X, Y1, Y2 being set
for f1 being Function of X,Y1
for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X)