for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds
g * d = id T