x .--> S = {[x,S]} by FUNCT_4:82;
hence {[x,S]} is 1-sorted-yielding ; :: thesis: verum