let S be OrderSortedSign; for z being non empty set
for CH being ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S holds ConstOSA (S,z,CH) is order-sorted
let z be non empty set ; for CH being ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S holds ConstOSA (S,z,CH) is order-sorted
let CH be ManySortedFunction of ((ConstOSSet (S,z)) #) * the Arity of S,(ConstOSSet (S,z)) * the ResultSort of S; ConstOSA (S,z,CH) is order-sorted
the Sorts of (ConstOSA (S,z,CH)) = ConstOSSet (S,z)
by Def18;
hence
ConstOSA (S,z,CH) is order-sorted
by Th17; verum