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 ;

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) ) )

hence
rng (p ^' q) = (rng p) \/ (rng q)
by TARSKI:2; :: thesis: verum( ( 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) ) )

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;

end;hereby :: thesis: ( x in (rng p) \/ (rng q) implies x in rng (p ^' q) )

assume
x in (rng p) \/ (rng q)
; :: thesis: 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;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

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;

end;

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;then len p in dom p by FINSEQ_3:25;

hence contradiction by A3, A11, A10, A15, FUNCT_1:def 3; :: thesis: verum

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;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