let k, m, n be Nat; :: thesis: ( n <= m implies (m --> k) | n = n --> k )
assume n <= m ; :: thesis: (m --> k) | n = n --> k
then Segm n c= Segm m by NAT_1:39;
then n /\ m = n by XBOOLE_1:28;
hence (m --> k) | n = n --> k by FUNCOP_1:12; :: thesis: verum