theorem Th45: :: YELLOW18:45

for A being category
for a, b being Object of A
for F1, F2 being Function st F1 in the Arrows of (Concretized A) . (a,b) & F2 in the Arrows of (Concretized A) . (a,b) & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] holds
F1 = F2