assume not b |-> a is positive ; :: thesis: contradiction
then consider k being Nat such that
A1: ( k in dom (b |-> a) & (b |-> a) . k <= 0 ) ;
thus contradiction by A1, FINSEQ_2:57; :: thesis: verum