for x being object st x in rng <*S1*> holds
x is 1-sorted

proof

let x be object ; :: thesis: ( x in rng <*S1*> implies x is 1-sorted )
assume x in rng <*S1*> ; :: thesis: x is 1-sorted
then x in {S1} by FINSEQ_1:38;
hence x is 1-sorted by TARSKI:def 1; :: thesis: verum

end;

hence <*S1*> is 1-sorted-yielding ; :: thesis: verum