for f being operation of A holds f is_exactly_partitable_wrt Class (LimDomRel A) by Th23;
hence ex b₁ being a_partition of the carrier of A st
for f being operation of A holds f is_exactly_partitable_wrt b₁ ; :: thesis: verum