defpred S1[ Nat, set , set ] means $3 = (modetrans ($2,S,(diff_SP ($1,S,T)))) `| Z;
A1:
for n being Nat
for x being set ex y being set st S1[n,x,y]
;
ex g being Function st
( dom g = NAT & g . 0 = f | Z & ( for n being Nat holds S1[n,g . n,g . (n + 1)] ) )
from RECDEF_1:sch 1(A1);
hence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (modetrans ((b1 . i),S,(diff_SP (i,S,T)))) `| Z ) )
; verum