defpred S1[ object , object ] means for i being Nat st i = $1 holds
$2 = diameter (S . i);
A1: for x being object st x in NAT holds
ex y being object st
( y in REAL & S1[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in REAL & S1[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )
then reconsider i = x as Nat ;
take diameter (S . i) ; :: thesis: ( diameter (S . i) in REAL & S1[x, diameter (S . i)] )
thus ( diameter (S . i) in REAL & S1[x, diameter (S . i)] ) by XREAL_0:def 1; :: thesis: verum
end;
consider f being sequence of REAL such that
A2: for x being object st x in NAT holds
S1[x,f . x] from FUNCT_2:sch 1(A1);
 take f ; :: thesis: for i being Nat holds f . i = diameter (S . i)
let i be Nat; :: thesis: f . i = diameter (S . i)
i in NAT by ORDINAL1:def 12;
hence f . i = diameter (S . i) by A2; :: thesis: verum