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

proof

assume x in dom (f ^ g) ; :: thesis: ( x in dom f or (x + 1) - (len f) in dom g )
then A1: x in Segm ((len f) + (len g)) by Def1;

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

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

then x in Segm (len f) by NAT_1:44;
hence ( x in dom f or (x + 1) - (len f) in dom g ) ; :: thesis: verum

end;

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

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

end;

end;

end;

( ( x in dom f or (x + 1) - (len f) in dom g ) implies x in dom (f ^ g) )

proof

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

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

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

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

end;

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

then (x + 1) - (len f) <= len g by FINSEQ_3:25;
then ((x + 1) - (len f)) + (len f) <= (len g) + (len f) by XREAL_1:6;
then x < (len g) + (len f) by NAT_1:13;
then x in Segm ((len g) + (len f)) by NAT_1:44;
hence x in dom (f ^ g) by Def1; :: thesis: verum

end;

end;

end;

hence ( x in dom (f ^ g) iff ( x in dom f or (x + 1) - (len f) in dom g ) ) by L1; :: thesis: verum