let A be partial non-empty UAStr ; :: thesis: Class (LimDomRel A) is a_partition of A
thus for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A) by Th25; :: according to PUA2MSS1:def 11 :: thesis: verum