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 b1 in (dom f) \/ (seq ((len f),(len g))) )
assume A1: a in dom (f ^ g) ; :: thesis: b1 in (dom f) \/ (seq ((len f),(len g)))
reconsider i = a as Element of NAT by A1;
A2: 1 <= i by ;
A3: i <= len (f ^ g) by ;
per cases ( i <= len f or len f < i ) ;
suppose A4: i <= len f ; :: thesis: b1 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 ;
hence a in (dom f) \/ (seq ((len f),(len g))) by A5; :: thesis: verum
end;
suppose A6: len f < i ; :: thesis: b1 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 ;
(len f) + 1 <= i by ;
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 ;
suppose A10: a in dom f ; :: thesis: a in dom (f ^ g)
then reconsider i = a as Element of NAT ;
A11: 1 <= i by ;
A12: len f <= len (f ^ g) by CALCUL_1:6;
i <= len f by ;
then i <= len (f ^ g) by ;
hence a in dom (f ^ g) by ; :: 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 ;
then A14: i <= len (f ^ g) by FINSEQ_1:22;
A15: 1 <= 1 + (len f) by NAT_1:11;
1 + (len f) <= i by ;
then 1 <= i by ;
hence a in dom (f ^ g) by ; :: thesis: verum
end;
end;