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 A3: ( ( 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));
for x being object st x in the carrier of (ConPoset (P,P)) holds
h1 . x = h2 . x

proof

let x be object ; :: 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 Lm24;
h1 . x = least_fix_point h by A3
.= h2 . x by A3 ;
hence h1 . x = h2 . x ; :: thesis: verum

end;

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