let P, Q be non empty strict chain-complete Poset; :: thesis: for f, g being Function of P,Q st f <= g & g <= f holds
f = g
let f, g be Function of P,Q; :: thesis: ( f <= g & g <= f implies f = g )
assume A1: ( f <= g & g <= f ) ; :: thesis: f = g
for x being object st x in the carrier of P holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in the carrier of P implies f . x = g . x )
assume x in the carrier of P ; :: thesis: f . x = g . x
then reconsider p = x as Element of P ;
set q1 = f . p;
set q2 = g . p;
A2: f . p <= g . p by A1, YELLOW_2:9;
g . p <= f . p by A1, YELLOW_2:9;
hence f . x = g . x by A2, ORDERS_2:2; :: thesis: verum

end;

hence f = g by FUNCT_2:12; :: thesis: verum