theorem Th68: :: FUNCT_3:68

for X being set
for f, g being Function st dom f = X & dom g = X holds
<:f,g:> = [:f,g:] * (delta X)