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 Def20;
hence ConstOSA S,z,CH is order-sorted by Th17; :: thesis: verum