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)
len q <> 0 by A2;
then 0 < len q ;
then 0 + 1 <= len q by NAT_1:13;
then A4: 1 + 1 <= (len q) + 1 by XREAL_1:9;
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

let x be set ; :: 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 A6: x in (rng p) \/ (rng (2,(len q) -cut q)) by FINSEQ_1:44;
A7: 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 A6, XBOOLE_0:def 3;
hence x in (rng p) \/ (rng q) by A7, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

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

len p <> 0 by A1;
then 0 < len p ;
then 0 + 1 <= len p by NAT_1:13;
then len p in dom p by FINSEQ_3:27;
hence contradiction by A3, A10, A11, A13, FUNCT_1:def 5; :: thesis: verum

end;

suppose 1 < y ; :: thesis: contradiction

then 1 + 1 <= y by NAT_1:13;
then consider i being Element of NAT such that
A14: ( 1 <= i & i < len q & y = i + 1 ) by A12, Th1;
A15: ( 0 + 1 <= i & i <= len (2,(len q) -cut q) ) by A5, A14, NAT_1:13;
then consider j being Element of NAT such that
A16: ( 0 <= j & j < len (2,(len q) -cut q) & i = j + 1 ) by Th1;
A17: (2,(len q) -cut q) . (j + 1) = q . ((1 + 1) + j) by A4, A16, Lm2
.= q . y by A14, A16 ;
i in dom (2,(len q) -cut q) by A15, FINSEQ_3:27;
hence contradiction by A10, A11, A16, A17, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

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