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