let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds
d * g = id S
let g be Function of S,T; :: thesis: for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds
d * g = id S
let d be Function of T,S; :: thesis: ( ( for s being Element of S holds g . s is_maximum_of d " {s} ) implies d * g = id S )
assume A1: for s being Element of S holds g . s is_maximum_of d " {s} ; :: thesis: d * g = id S
for s being Element of S holds (d * g) . s = s

proof

let s be Element of S; :: thesis: (d * g) . s = s
g . s is_maximum_of d " {s} by A1;
then ( g . s = sup (d " {s}) & sup (d " {s}) in d " {s} ) ;
then d . (g . s) in {s} by FUNCT_2:38;
then d . (g . s) = s by TARSKI:def 1;
hence (d * g) . s = s by FUNCT_2:15; :: thesis: verum

end;

hence d * g = id S by FUNCT_2:124; :: thesis: verum