f1 ^' f2 is FinSequence of NAT ;
hence f1 ^' f2 is IL-FinSequence of S by Def34; :: thesis: verum