defpred S1[ Nat, object ] means $2 = len (s . $1);
A1: for k being Element of NAT ex x being Element of NAT st S1[k,x] ;
consider IT being Function of NAT,NAT such that
A2: for k being Element of NAT holds S1[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;