:: deftheorem defines .--> FUNCOP_1:def 7 :
for a, b, c being object holds (a,b) .--> c = {[a,b]} --> c;