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

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