set X = the carrier of (ConPoset (P,P));
set Y = the carrier of P;
defpred S₁[ object , object ] means for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h & g = $1 holds
$2 = least_fix_point h;
A1: for x being object st x in the carrier of (ConPoset (P,P)) holds
ex y being object st
( y in the carrier of P & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (ConPoset (P,P)) implies ex y being object st
( y in the carrier of P & S₁[x,y] ) )
assume x in the carrier of (ConPoset (P,P)) ; :: thesis: ex y being object st
( y in the carrier of P & S₁[x,y] )
then reconsider x = x as Element of (ConPoset (P,P)) ;
reconsider h = x as continuous Function of P,P by Lm24;
take least_fix_point h ; :: thesis: ( least_fix_point h in the carrier of P & S₁[x, least_fix_point h] )
thus ( least_fix_point h in the carrier of P & S₁[x, least_fix_point h] ) ; :: thesis: verum

end;

consider IT being Function of the carrier of (ConPoset (P,P)), the carrier of P such that
A2: for x being object st x in the carrier of (ConPoset (P,P)) holds
S₁[x,IT . x] from FUNCT_2:sch 1(A1);
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
IT . g = least_fix_point h by A2;
hence ex b₁ being Function of (ConPoset (P,P)),P st
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b₁ . g = least_fix_point h ; :: thesis: verum