for x being object st x in rng (X --> S) holds
x is 1-sorted

proof

let x be object ; :: thesis: ( x in rng (X --> S) implies x is 1-sorted )

per cases ( X <> {} or X = {} ) ;

suppose A1: X <> {} ; :: thesis: ( x in rng (X --> S) implies x is 1-sorted )

assume x in rng (X --> S) ; :: thesis: x is 1-sorted
then x in {S} by A1, FUNCOP_1:8;
hence x is 1-sorted by TARSKI:def 1; :: thesis: verum

end;

suppose X = {} ; :: thesis: ( x in rng (X --> S) implies x is 1-sorted )

hence ( x in rng (X --> S) implies x is 1-sorted ) ; :: thesis: verum

end;

end;

end;

hence X --> S is 1-sorted-yielding ; :: thesis: verum