theorem Th23: :: PUA2MSS1:24

for A being partial non-empty UAStr
for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A)