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

assume len p = 0 ; :: thesis: q = p ^ q

then p = {} ;

hence q = p ^ q by FINSEQ_1:34; :: thesis: verum