let i, j, k be set ; :: thesis: ((i,j) :-> k) . (i,j) = k
thus ((i,j) :-> k) . (i,j) = ([i,j] .--> k) . [i,j]
.= k by FUNCOP_1:72 ; :: thesis: verum