reconsider b = b as set by TARSKI:1;
the_value_of ((Seg a) --> b) = b by FUNCOP_1:79;
hence the_value_of (a |-> b) = b by FINSEQ_2:def 2; :: thesis: verum