let f, g be FinSequence; :: thesis: Seg (len (f ^ g)) = (Seg (len f)) \/ (seq ((len f),(len g)))
thus Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def 3
.= (dom f) \/ (seq ((len f),(len g))) by CALCUL_2:9
.= (Seg (len f)) \/ (seq ((len f),(len g))) by FINSEQ_1:def 3 ; :: thesis: verum