theorem :: FUNCOP_1:71

for a, b, c being object holds ((a,b) .--> c) . (a,b) = c