f in the carrier of s * by FINSEQ_1:def 11;
hence [f,t] is Element of [:(the carrier of s * ),the carrier of s:] by ZFMISC_1:106; :: thesis: verum