theorem Th7: :: ALTCAT_1:13

for o being set holds FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o)