for x being object st x in rng (p ^ q) holds
x is 1-sorted

proof

let x be object ; :: thesis: ( x in rng (p ^ q) implies x is 1-sorted )
assume x in rng (p ^ q) ; :: thesis: x is 1-sorted
then x in (rng p) \/ (rng q) by FINSEQ_1:31;

per cases then ( x in rng p or x in rng q ) by XBOOLE_0:def 3;

suppose x in rng p ; :: thesis: x is 1-sorted

hence x is 1-sorted by Def11; :: thesis: verum

end;

suppose x in rng q ; :: thesis: x is 1-sorted

hence x is 1-sorted by Def11; :: thesis: verum

end;

end;

end;

hence p ^ q is 1-sorted-yielding ; :: thesis: verum