defpred S₁[ Nat, object ] means $2 = len (s . $1);
A1: for k being Element of NAT ex x being Element of NAT st S₁[k,x] ;
consider IT being Function of NAT,NAT such that
A2: for k being Element of NAT holds S₁[k,IT . k] from FUNCT_2:sch 3(A1);
take IT ; :: thesis: for n being Nat holds IT . n = len (s . n)

hereby :: thesis: verum

let n be Nat; :: thesis: IT . n = len (s . n)
n is Element of NAT by ORDINAL1:def 12;
hence IT . n = len (s . n) by A2; :: thesis: verum

end;