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

proof

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

end;

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