let h1, h2 be Function of (ConPoset (P,P)),P; :: thesis:
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:
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

let x be object ; :: thesis:
assume x in the carrier of (ConPoset (P,P)) ; :: thesis:
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:

end;