let f, g be FinSequence; :: thesis:

let a be object ; :: thesis:
assume A1: a in dom (f ^ g) ; :: thesis:
reconsider i = a as Element of NAT by A1;
A2: 1 <= i by A1, FINSEQ_3:25;
A3: i <= len (f ^ g) by A1, FINSEQ_3:25;

suppose A4: i <= len f ; :: thesis:

A5: dom f c= (dom f) \/ (seq ((len f),(len g))) by XBOOLE_1:7;
i in dom f by A2, A4, FINSEQ_3:25;
hence a in (dom f) \/ (seq ((len f),(len g))) by A5; :: thesis:

end;

suppose A6: len f < i ; :: thesis:

A7: seq ((len f),(len g)) c= (dom f) \/ (seq ((len f),(len g))) by XBOOLE_1:7;
A8: i <= (len f) + (len g) by A3, FINSEQ_1:22;
(len f) + 1 <= i by A6, NAT_1:13;
then a in seq ((len f),(len g)) by A8;
hence a in (dom f) \/ (seq ((len f),(len g))) by A7; :: thesis:

end;

end;

end;

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

per cases by A9, XBOOLE_0:def 3;

suppose A10: a in dom f ; :: thesis:

then reconsider i = a as Element of NAT ;
A11: 1 <= i by A10, FINSEQ_3:25;
A12: len f <= len (f ^ g) by CALCUL_1:6;
i <= len f by A10, FINSEQ_3:25;
then i <= len (f ^ g) by A12, XXREAL_0:2;
hence a in dom (f ^ g) by A11, FINSEQ_3:25; :: thesis:

end;

suppose A13: a in seq ((len f),(len g)) ; :: thesis:

then reconsider i = a as Element of NAT ;
i <= (len g) + (len f) by A13, Th1;
then A14: i <= len (f ^ g) by FINSEQ_1:22;
A15: 1 <= 1 + (len f) by NAT_1:11;
1 + (len f) <= i by A13, Th1;
then 1 <= i by A15, XXREAL_0:2;
hence a in dom (f ^ g) by A14, FINSEQ_3:25; :: thesis:

end;

end;