theorem :: FUNCT_4:80

for i, j, k being object holds ((i,j) :-> k) . (i,j) = k by FUNCOP_1:71;