theorem Th82: :: FUNCOP_1:82

for x, y being object holds x .--> y is_isomorphism_of {[x,x]},{[y,y]}