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 ;
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 ; :: 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 ;
A11: not x in rng p by ;
reconsider y = y as Element of NAT by A9;
A12: 1 <= y by ;
A13: y <= len q by ;
A14: not x in rng ((2,(len q)) -cut q) by ;
per cases ( y = 1 or 1 < y ) by ;
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 ;
A19: i <= len ((2,(len q)) -cut q) by ;
then A20: i in dom ((2,(len q)) -cut q) by ;
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 ;
((2,(len q)) -cut q) . (j + 1) = q . ((1 + 1) + j) by A4, A21, Lm2
.= q . y by ;
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