reconsider f = SCM-Compile . term as sequence of ( the InstructionsF of SCM ^omega) by FUNCT_2:66;
f . (In (aux,NAT)) in the InstructionsF of SCM ^omega ;
hence (SCM-Compile . term) . aux is XFinSequence of the InstructionsF of SCM by AFINSQ_1:def 7; :: thesis: verum