let S be OrderSortedSign; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum