let D be non empty set ; :: thesis: for p, q being FinSequence of D st len p = 0 holds
q = p ^ q
let p, q be FinSequence of D; :: thesis: ( len p = 0 implies q = p ^ q )
assume len p = 0 ; :: thesis: q = p ^ q
then p = <*> D
.= {} ;
hence q = p ^ q by FINSEQ_1:34; :: thesis: verum