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 set ; :: 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 A1: x in (rng p) \/ (rng (2,(len q) -cut q)) by FINSEQ_1:44;
A2: rng (2,(len q) -cut q) c= rng q by Th11;
( x in rng p or x in rng (2,(len q) -cut q) ) by A1, XBOOLE_0:def 3;
hence x in (rng p) \/ (rng q) by A2, XBOOLE_0:def 3; :: thesis: verum