let f be XFinSequence; :: thesis: for g being FinSequence holds
( len (f ^ g) = (len f) + (len g) & len (g ^ f) = (len f) + (len g) )
let g be FinSequence; :: thesis: ( len (f ^ g) = (len f) + (len g) & len (g ^ f) = (len f) + (len g) )
Seg ((len f) + (len g)) = dom (g ^ f) by Def2
.= Seg (len (g ^ f)) by FINSEQ_1:def 3 ;
hence ( len (f ^ g) = (len f) + (len g) & len (g ^ f) = (len f) + (len g) ) by Def1, FINSEQ_1:6; :: thesis: verum