let S, T be non empty Poset; :: thesis: 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
let g be Function of S,T; :: thesis: 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
let d be Function of T,S; :: thesis: ( ( for t being Element of T holds d . t is_minimum_of g " {t} ) implies g * d = id T )
assume A1: for t being Element of T holds d . t is_minimum_of g " {t} ; :: thesis: g * d = id T
for t being Element of T holds (g * d) . t = t
proof
let t be Element of T; :: thesis: (g * d) . t = t
d . t is_minimum_of g " {t} by A1;
then ( d . t = inf (g " {t}) & inf (g " {t}) in g " {t} ) ;
then g . (d . t) in {t} by FUNCT_2:38;
then g . (d . t) = t by TARSKI:def 1;
hence (g * d) . t = t by FUNCT_2:15; :: thesis: verum
end;
hence g * d = id T by FUNCT_2:124; :: thesis: verum