defpred S_{1}[ 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_{1}[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_{1}[n,g . n,g . (n + 1)] ) )
from RECDEF_1:sch 3(A2);

hence ex b_{1} being FinSequence st

( len b_{1} = len f & b_{1} . 1 = naming (V,A,(f . (len f)),a) & ( for n being Nat st 1 <= n & n < len b_{1} holds

b_{1} . (n + 1) = naming (V,A,(f . ((len f) - n)),(b_{1} . n)) ) )
by A1; :: thesis: verum

A2: for n being Nat st 1 <= n & n < len f holds

for x being set ex y being set st S

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

hence ex b

( len b

b