let f be FinSequence; :: thesis: for g being XFinSequence holds dom (f \/ (Shift (g,((len f) + 1)))) = Seg ((len f) + (len g))
let g be XFinSequence; :: thesis: dom (f \/ (Shift (g,((len f) + 1)))) = Seg ((len f) + (len g))
A0: dom (f \/ (Shift (g,((len f) + 1)))) = (dom f) \/ (dom (Shift (g,((len f) + 1)))) by XTUPLE_0:23;
for x being object holds
( x in dom (f \/ (Shift (g,((len f) + 1)))) iff x in Seg ((len f) + (len g)) )

proof

let x be object ; :: thesis: ( x in dom (f \/ (Shift (g,((len f) + 1)))) iff x in Seg ((len f) + (len g)) )
C1: ( x in dom (f \/ (Shift (g,((len f) + 1)))) implies x in Seg ((len f) + (len g)) )

proof

assume D1: x in dom (f \/ (Shift (g,((len f) + 1)))) ; :: thesis: x in Seg ((len f) + (len g))
then reconsider x = x as Nat ;

per cases ( x in dom f or x in dom (Shift (g,((len f) + 1))) ) by A0, D1, XBOOLE_0:def 3;

suppose x in dom f ; :: thesis: x in Seg ((len f) + (len g))

then ( 1 <= x & x <= len f & (len f) + (len g) >= (len f) + 0 ) by FINSEQ_3:25, XREAL_1:6;
then ( 1 <= x & x <= (len f) + (len g) ) by XXREAL_0:2;
hence x in Seg ((len f) + (len g)) ; :: thesis: verum

end;

suppose x in dom (Shift (g,((len f) + 1))) ; :: thesis: x in Seg ((len f) + (len g))

then x in { (m + ((len f) + 1)) where m is Nat : m in dom g } by VALUED_1:def 12;
then consider m being Nat such that
E1: ( x = m + ((len f) + 1) & m in dom g ) ;
m in Segm (len g) by E1;
then m < len g by NAT_1:44;
then m + 1 <= len g by NAT_1:13;
then ( 0 + 1 <= ((len f) + m) + 1 & (m + 1) + (len f) <= (len g) + (len f) ) by XREAL_1:6;
hence x in Seg ((len f) + (len g)) by E1; :: thesis: verum

end;

end;

end;

( x in Seg ((len f) + (len g)) implies x in dom (f \/ (Shift (g,((len f) + 1)))) )

proof

assume C1: x in Seg ((len f) + (len g)) ; :: thesis: x in dom (f \/ (Shift (g,((len f) + 1))))
then reconsider x = x as Nat ;
C2: ( 1 <= x & x <= (len f) + (len g) ) by C1, FINSEQ_1:1;

per cases ( ( 1 <= x & x <= len f ) or x > len f ) by C1, FINSEQ_1:1;

suppose ( 1 <= x & x <= len f ) ; :: thesis: x in dom (f \/ (Shift (g,((len f) + 1))))

then x in dom f by FINSEQ_3:25;
hence x in dom (f \/ (Shift (g,((len f) + 1)))) by A0, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x > len f ; :: thesis: x in dom (f \/ (Shift (g,((len f) + 1))))

then x >= (len f) + 1 by NAT_1:13;
then D1: ( ((len f) + (len g)) - (len f) >= x - (len f) & x - (len f) >= ((len f) + 1) - (len f) ) by C2, XREAL_1:9;
then reconsider k = x - (len f) as non zero Nat ;
reconsider l = k - 1 as Nat ;
l + 1 in Seg (len g) by D1;
then l in Segm (len g) by NEWTON02:106;
then (x - ((len f) + 1)) + ((len f) + 1) in dom (Shift (g,((len f) + 1))) by VALUED_1:24;
hence x in dom (f \/ (Shift (g,((len f) + 1)))) by A0, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ( x in dom (f \/ (Shift (g,((len f) + 1)))) iff x in Seg ((len f) + (len g)) ) by C1; :: thesis: verum

end;

hence dom (f \/ (Shift (g,((len f) + 1)))) = Seg ((len f) + (len g)) by TARSKI:2; :: thesis: verum