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