let f be non empty XFinSequence; :: thesis: for g being FinSequence holds dom (f \/ (Shift (g,((len f) - 1)))) = Segm ((len f) + (len g))
let g be FinSequence; :: thesis: dom (f \/ (Shift (g,((len f) - 1)))) = Segm ((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 Segm ((len f) + (len g)) )

proof

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

proof

assume D1: x in dom (f \/ (Shift (g,((len f) - 1)))) ; :: thesis: x in Segm ((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 Segm ((len f) + (len g))

then ( x in Segm (len f) & (len f) + (len g) >= (len f) + 0 ) by XREAL_1:6;
then x < (len f) + (len g) by XXREAL_0:2, NAT_1:44;
hence x in Segm ((len f) + (len g)) by NAT_1:44; :: thesis: verum

end;

suppose x in dom (Shift (g,((len f) - 1))) ; :: thesis: x in Segm ((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 <= len g by E1, FINSEQ_3:25;
then m < (len g) + 1 by NAT_1:13;
then m + ((len f) - 1) < ((len g) + 1) + ((len f) - 1) by XREAL_1:6;
hence x in Segm ((len f) + (len g)) by NAT_1:44, E1; :: thesis: verum

end;

end;

end;

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

proof

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

per cases ( x < len f or x >= len f ) ;

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

then x in Segm (len f) by NAT_1:44;
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 D1: ( ((len f) + (len g)) - (len f) > x - (len f) & x - (len f) >= (len f) - (len f) ) by C1, NAT_1:44, XREAL_1:9;
then reconsider k = x - (len f) as Nat by INT_1:3;
k in Segm (len g) by D1, NAT_1:44;
then k + 1 in Seg (len g) by NEWTON02:106;
then x - ((len f) - 1) in dom g by FINSEQ_1:def 3;
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 Segm ((len f) + (len g)) ) by C1; :: thesis: verum

end;

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