let f, g be FinSequence; :: thesis: dom (f ^ g) = (dom f) \/ (seq ((len f),(len 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)

now :: thesis: for a being object st a in dom (f ^ g) holds

a in (dom f) \/ (seq ((len f),(len g)))

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)a in (dom f) \/ (seq ((len f),(len g)))

let a be object ; :: thesis: ( a in dom (f ^ g) implies b_{1} in (dom f) \/ (seq ((len f),(len g))) )

assume A1: a in dom (f ^ g) ; :: thesis: b_{1} 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;

end;assume A1: a in dom (f ^ g) ; :: thesis: b

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 )
;

end;

suppose A4:
i <= len f
; :: thesis: b_{1} 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;i in dom f by A2, A4, FINSEQ_3:25;

hence a in (dom f) \/ (seq ((len f),(len g))) by A5; :: thesis: verum

suppose A6:
len f < i
; :: thesis: b_{1} 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;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

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;

end;

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;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

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;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