let f, g be FinSequence; :: thesis: dom (f ^ g) = (dom f) \/ (seq (len f),(len g))

now

let a be set ; :: thesis: ( a in dom (f ^ g) implies b₁ in (dom f) \/ (seq (len f),(len g)) )
assume A1: a in dom (f ^ g) ; :: thesis: b₁ in (dom f) \/ (seq (len f),(len g))
reconsider i = a as Element of NAT by A1;
A2: ( 1 <= i & i <= len (f ^ g) ) by A1, FINSEQ_3:27;

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

suppose i <= len f ; :: thesis: b₁ in (dom f) \/ (seq (len f),(len g))

then A3: i in dom f by A2, FINSEQ_3:27;
dom f c= (dom f) \/ (seq (len f),(len g)) by XBOOLE_1:7;
hence a in (dom f) \/ (seq (len f),(len g)) by A3; :: thesis: verum

end;

suppose len f < i ; :: thesis: b₁ in (dom f) \/ (seq (len f),(len g))

then ( (len f) + 1 <= i & i <= (len f) + (len g) ) by A2, FINSEQ_1:35, NAT_1:13;
then A4: a in seq (len f),(len g) ;
seq (len f),(len g) c= (dom f) \/ (seq (len f),(len g)) by XBOOLE_1:7;
hence a in (dom f) \/ (seq (len f),(len g)) by A4; :: thesis: verum

end;

end;

end;

hence dom (f ^ g) c= (dom f) \/ (seq (len f),(len g)) by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: (dom f) \/ (seq (len f),(len g)) c= dom (f ^ g)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (dom f) \/ (seq (len f),(len g)) or a in dom (f ^ g) )
assume A5: a in (dom f) \/ (seq (len f),(len g)) ; :: thesis: a in dom (f ^ g)

per cases ( a in dom f or a in seq (len f),(len g) ) by A5, XBOOLE_0:def 3;

suppose A6: a in dom f ; :: thesis: a in dom (f ^ g)

then reconsider i = a as Element of NAT ;
A7: ( 1 <= i & i <= len f ) by A6, FINSEQ_3:27;
len f <= len (f ^ g) by CALCUL_1:6;
then i <= len (f ^ g) by A7, XXREAL_0:2;
hence a in dom (f ^ g) by A7, FINSEQ_3:27; :: thesis: verum

end;

suppose A8: a in seq (len f),(len g) ; :: thesis: a in dom (f ^ g)

then reconsider i = a as Element of NAT ;
A9: ( 1 + (len f) <= i & i <= (len g) + (len f) ) by A8, Th1;
then A10: i <= len (f ^ g) by FINSEQ_1:35;
1 <= 1 + (len f) by NAT_1:11;
then 1 <= i by A9, XXREAL_0:2;
hence a in dom (f ^ g) by A10, FINSEQ_3:27; :: thesis: verum

end;

end;