defpred S₁[ set , set ] means for i being natural number st i = $1 holds
$2 = diameter (S . i);
A1: for x being set st x in NAT holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
then reconsider i = x as Element of NAT ;
take diameter (S . i) ; :: thesis: ( diameter (S . i) in REAL & S₁[x, diameter (S . i)] )
thus ( diameter (S . i) in REAL & S₁[x, diameter (S . i)] ) ; :: thesis: verum

end;

consider f being Function of NAT ,REAL such that
A2: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for i being natural number holds f . i = diameter (S . i)
let i be natural number ; :: thesis: f . i = diameter (S . i)
i in NAT by ORDINAL1:def 13;
hence f . i = diameter (S . i) by A2; :: thesis: verum