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:87; :: thesis: verum