reconsider f = SCM-Compile . term as Function of NAT,( the Instructions of SCM ^omega) by FUNCT_2:121;
f . aux in the Instructions of SCM ^omega ;
hence (SCM-Compile . term) . aux is XFinSequence of the Instructions of SCM by AFINSQ_1:def 8; :: thesis: verum