let p, q be FinSequence; :: thesis: ( len p = 0 implies q = p ^ q )
assume len p = 0 ; :: thesis: q = p ^ q
then p = {} ;
hence q = p ^ q by FINSEQ_1:34; :: thesis: verum