let p, q be FinSequence; :: thesis: rng (p ^' q) c= (rng p) \/ (rng q)
set r = p ^' q;
set qc = (2,(len q)) -cut q;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (p ^' q) or x in (rng p) \/ (rng q) )
assume x in rng (p ^' q) ; :: thesis: x in (rng p) \/ (rng q)
then x in (rng p) \/ (rng ((2,(len q)) -cut q)) by FINSEQ_1:31;
then A1: ( x in rng p or x in rng ((2,(len q)) -cut q) ) by XBOOLE_0:def 3;
rng ((2,(len q)) -cut q) c= rng q by Th11;
hence x in (rng p) \/ (rng q) by A1, XBOOLE_0:def 3; :: thesis: verum