let p, q be FinSequence; :: thesis: ( p <> {} & q <> {} & p . (len p) = q . 1 implies rng (p ^' q) = (rng p) \/ (rng q) )
set r = p ^' q;
set qc = (2,(len q)) -cut q;
assume that
A1: p <> {} and
A2: q <> {} and
A3: p . (len p) = q . 1 ; :: thesis: rng (p ^' q) = (rng p) \/ (rng q)
0 + 1 <= len q by A2, NAT_1:13;
then A4: 1 + 1 <= (len q) + 1 by XREAL_1:7;
then (len ((2,(len q)) -cut q)) + (1 + 1) = (len q) + 1 by Lm2;
then A5: ((len ((2,(len q)) -cut q)) + 1) + 1 = (len q) + 1 ;

now :: thesis: for x being object holds
( ( x in rng (p ^' q) implies x in (rng p) \/ (rng q) ) & ( x in (rng p) \/ (rng q) implies x in rng (p ^' q) ) )

let x be object ; :: thesis: ( ( x in rng (p ^' q) implies x in (rng p) \/ (rng q) ) & ( x in (rng p) \/ (rng q) implies x in rng (p ^' q) ) )

hereby :: thesis: ( x in (rng p) \/ (rng q) implies x in rng (p ^' 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 A6: ( 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 A6, XBOOLE_0:def 3; :: thesis: verum

end;

assume x in (rng p) \/ (rng q) ; :: thesis: x in rng (p ^' q)
then A7: ( x in rng p or x in rng q ) by XBOOLE_0:def 3;
assume not x in rng (p ^' q) ; :: thesis: contradiction
then A8: not x in (rng p) \/ (rng ((2,(len q)) -cut q)) by FINSEQ_1:31;
then consider y being object such that
A9: y in dom q and
A10: x = q . y by A7, FUNCT_1:def 3, XBOOLE_0:def 3;
A11: not x in rng p by A8, XBOOLE_0:def 3;
reconsider y = y as Element of NAT by A9;
A12: 1 <= y by A9, FINSEQ_3:25;
A13: y <= len q by A9, FINSEQ_3:25;
A14: not x in rng ((2,(len q)) -cut q) by A8, XBOOLE_0:def 3;

per cases ( y = 1 or 1 < y ) by A12, XXREAL_0:1;

suppose A15: y = 1 ; :: thesis: contradiction

0 + 1 <= len p by A1, NAT_1:13;
then len p in dom p by FINSEQ_3:25;
hence contradiction by A3, A11, A10, A15, FUNCT_1:def 3; :: thesis: verum

end;

suppose 1 < y ; :: thesis: contradiction

then 1 + 1 <= y by NAT_1:13;
then consider i being Nat such that
A16: 1 <= i and
A17: i < len q and
A18: y = i + 1 by A13, Th1;
A19: i <= len ((2,(len q)) -cut q) by A5, A17, NAT_1:13;
then A20: i in dom ((2,(len q)) -cut q) by A16, FINSEQ_3:25;
0 + 1 <= i by A16;
then consider j being Nat such that
0 <= j and
A21: j < len ((2,(len q)) -cut q) and
A22: i = j + 1 by A19, Th1;
((2,(len q)) -cut q) . (j + 1) = q . ((1 + 1) + j) by A4, A21, Lm2
.= q . y by A18, A22 ;
hence contradiction by A14, A10, A22, A20, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

hence rng (p ^' q) = (rng p) \/ (rng q) by TARSKI:2; :: thesis: verum