theorem Th81: :: FUNCT_4:81

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