theorem :: FUNCT_4:79

for i, j, k being object holds (i,j) :-> k = [i,j] .--> k ;