set X = the carrier of (ConPoset P,P);
set Y = the carrier of P;
defpred S₁[ set , set ] 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 set st x in the carrier of (ConPoset P,P) holds
ex y being set st
( y in the carrier of P & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier of (ConPoset P,P) implies ex y being set st
( y in the carrier of P & S₁[x,y] ) )
assume x in the carrier of (ConPoset P,P) ; :: thesis: ex y being set 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 LemCastFunc01;
take y = least_fix_point h; :: thesis: ( y in the carrier of P & S₁[x,y] )
thus ( y in the carrier of P & S₁[x,y] ) ; :: thesis: verum

end;

consider IT being Function of the carrier of (ConPoset P,P),the carrier of P such that
A2: for x being set 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