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 Th23; :: according to PUA2MSS1:def 10 :: thesis: verum