set X = the carrier of P;
set Y = the carrier of Q;
defpred S₁[ set , set ] means for p being Element of P
for M being non empty Chain of Q st p = $1 & M = F -image p holds
$2 = sup M;
A1: for x being set st x in the carrier of P holds
ex y being set st
( y in the carrier of Q & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier of P implies ex y being set st
( y in the carrier of Q & S₁[x,y] ) )
assume x in the carrier of P ; :: thesis: ex y being set st
( y in the carrier of Q & S₁[x,y] )
then reconsider x = x as Element of P ;
reconsider a = F -image x as non empty Chain of Q ;
set y = sup a;
take sup a ; :: thesis: ( sup a in the carrier of Q & S₁[x, sup a] )
thus ( sup a in the carrier of Q & S₁[x, sup a] ) ; :: thesis: verum

end;

consider IT being Function of the carrier of P, the carrier of Q such that
A2: for x being set st x in the carrier of P holds
S₁[x,IT . x] from FUNCT_2:sch 1(A1);
for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
IT . p = sup M by A2;
hence ex b₁ being Function of P,Q st
for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b₁ . p = sup M ; :: thesis: verum