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

now :: thesis: for a being object st a in dom (f ^ g) holds
a in (dom f) \/ (seq ((len f),(len g)))

let a be object ; :: 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 by A1, FINSEQ_3:25;
A3: i <= len (f ^ g) by A1, FINSEQ_3:25;

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

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

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: verum

end;

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

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: verum

end;

end;

end;

hence dom (f ^ g) c= (dom f) \/ (seq ((len f),(len g))) ; :: according to XBOOLE_0:def 10 :: thesis: (dom f) \/ (seq ((len f),(len g))) c= dom (f ^ g)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (dom f) \/ (seq ((len f),(len g))) or a in dom (f ^ g) )
assume A9: 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 A9, XBOOLE_0:def 3;

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

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: verum

end;

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

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: verum

end;

end;