defpred S₁[ 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 S<sub>1</sub>[n,x,y] ;
ex g being Function st
( dom g = NAT & g . 0 = f | Z & ( for n being Nat holds S<sub>1</sub>[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 1(A1);
hence ex b<sub>1</sub> being Function st
( dom b<sub>1</sub> = NAT & b<sub>1</sub> . 0 = f | Z & ( for i being Nat holds b<sub>1</sub> . (i + 1) = (modetrans ((b<sub>1</sub> . i),S,(diff_SP (i,S,T)))) `| Z ) ) ; :: thesis: verum