theorem Th82: :: COMPUT_1:83

for i, j, k being Nat
for f being NAT * -defined to-naturals homogeneous len-total 2 -ary Function holds ((1,2)->(1,?,2) f) . <*i,j,k*> = f . <*i,k*>