reconsider h = g " as m -element complex-valued FinSequence ;
f (#) h is min (n,m) -element ;
hence f /" g is min (n,m) -element by VALUED_1:def 10; :: thesis: verum