(Seg a) --> b is constant ;
hence a |-> b is constant by FINSEQ_2:def 2; :: thesis: verum