theorem Th72: :: CAT_8:72

for C1, C2 being category holds C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2