let p, q be FinSequence; ( 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
; 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 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 ;
( ( x in rng (p ^' q) implies x in (rng p) \/ (rng q) ) & ( x in (rng p) \/ (rng q) implies x in rng (p ^' q) ) )assume
x in (rng p) \/ (rng q)
;
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)
;
contradictionthen 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
1
< y
;
contradictionthen
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;
verum end; end;
hence
rng (p ^' q) = (rng p) \/ (rng q)
by TARSKI:2; verum