let f be S -Terms X -valued Function; :: thesis: f is finite-yielding
for x being set st x in rng f holds
x is finite ;
hence f is finite-yielding ; :: thesis: verum