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:87 ; :: thesis: verum