:: deftheorem Def10 defines sort-preserving AOFA_L00:def 10 :
for J being non empty set
for Q being ManySortedSet of J
for Y being set
for f being Function of [:(Union Q),Y:],(Union Q) holds
( f is sort-preserving iff for j being Element of J holds f .: [:(Q . j),Y:] c= Q . j );