defpred S₁[ Nat, object , object ] means $3 = naming (V,A,(f . ((len f) - $1)),$2);
A2: for n being Nat st 1 <= n & n < len f holds
for x being set ex y being set st S₁[n,x,y] ;
ex g being FinSequence st
( len g = len f & ( g . 1 = naming (V,A,(f . (len f)),a) or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds
S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 3(A2);
hence ex b₁ being FinSequence st
( len b₁ = len f & b₁ . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b₁ holds
b₁ . (n + 1) = naming (V,A,(f . ((len f) - n)),(b₁ . n)) ) ) by A1; :: thesis: verum