let h1, h2 be Function of (ConPoset P,P),P; :: thesis: ( ( for g being Element of (ConPoset P,P)
for h being continuous Function of P,P st g = h holds
h1 . g = least_fix_point h ) & ( for g being Element of (ConPoset P,P)
for h being continuous Function of P,P st g = h holds
h2 . g = least_fix_point h ) implies h1 = h2 )
assume A1: ( ( for g being Element of (ConPoset P,P)
for h being continuous Function of P,P st g = h holds
h1 . g = least_fix_point h ) & ( for g being Element of (ConPoset P,P)
for h being continuous Function of P,P st g = h holds
h2 . g = least_fix_point h ) ) ; :: thesis: h1 = h2
set X = the carrier of (ConPoset P,P);
set Y = the carrier of P;
for x being set st x in the carrier of (ConPoset P,P) holds
h1 . x = h2 . x

proof

let x be set ; :: thesis: ( x in the carrier of (ConPoset P,P) implies h1 . x = h2 . x )
assume x in the carrier of (ConPoset P,P) ; :: thesis: h1 . x = h2 . x
then reconsider g = x as Element of (ConPoset P,P) ;
reconsider h = g as continuous Function of P,P by LemCastFunc01;
h1 . x = least_fix_point h by A1
.= h2 . x by A1 ;
hence h1 . x = h2 . x ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:18; :: thesis: verum