let f be FinSequence; :: thesis: for g being XFinSequence
for x being Nat holds
( x in dom (f ^ g) iff ( x in dom f or x - ((len f) + 1) in dom g ) )
let g be XFinSequence; :: thesis: for x being Nat holds
( x in dom (f ^ g) iff ( x in dom f or x - ((len f) + 1) in dom g ) )
let x be Nat; :: thesis: ( x in dom (f ^ g) iff ( x in dom f or x - ((len f) + 1) in dom g ) )
thus ( not x in dom (f ^ g) or x in dom f or x - ((len f) + 1) in dom g ) :: thesis: ( ( x in dom f or x - ((len f) + 1) in dom g ) implies x in dom (f ^ g) )

proof

assume x in dom (f ^ g) ; :: thesis: ( x in dom f or x - ((len f) + 1) in dom g )
then x in Seg ((len f) + (len g)) by Def2;
then A1: ( 1 <= x & x <= (len f) + (len g) ) by FINSEQ_1:1;

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

suppose x <= len f ; :: thesis: ( x in dom f or x - ((len f) + 1) in dom g )

then x in Seg (len f) by A1;
hence ( x in dom f or x - ((len f) + 1) in dom g ) by FINSEQ_1:def 3; :: thesis: verum

end;

suppose len f < x ; :: thesis: ( x in dom f or x - ((len f) + 1) in dom g )

then (len f) + 1 <= x by NAT_1:13;
then ((len f) + 1) - ((len f) + 1) <= x - ((len f) + 1) by XREAL_1:9;
then reconsider y = x - ((len f) + 1) as Nat by INT_1:3;
(y + ((len f) + 1)) - (len f) <= ((len f) + (len g)) - (len f) by A1, XREAL_1:9;
then y + 1 <= len g ;
then y < len g by NAT_1:13;
then y in Segm (len g) by NAT_1:44;
hence ( x in dom f or x - ((len f) + 1) in dom g ) ; :: thesis: verum

end;

end;

end;

assume ( x in dom f or x - ((len f) + 1) in dom g ) ; :: thesis: x in dom (f ^ g)

per cases then ( x in dom f or x - ((len f) + 1) in dom g ) ;

suppose x in dom f ; :: thesis: x in dom (f ^ g)

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

end;

suppose B1: x - ((len f) + 1) in dom g ; :: thesis: x in dom (f ^ g)

then reconsider y = x - ((len f) + 1) as Nat ;
y in Segm (len g) by B1;
then y < len g by NAT_1:44;
then y + 1 <= len g by NAT_1:13;
then ( 1 + 0 <= 1 + (y + (len f)) & (y + 1) + (len f) <= (len g) + (len f) ) by XREAL_1:6;
then x in Seg ((len g) + (len f)) ;
hence x in dom (f ^ g) by Def2; :: thesis: verum

end;

end;