defpred S₁[ Nat, set , set ] means $3 = [:$2,(X . ($1 + 1)):];
A1: for n being Nat st 1 <= n & n < m holds
for x being set ex y being set st S₁[n,x,y] ;
consider p being FinSequence such that
A2: ( len p = m & ( p . 1 = X . 1 or m = 0 ) & ( for n being Nat st 1 <= n & n < m holds
S₁[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 3(A1);
reconsider p = p as m -element FinSequence by A2, CARD_1:def 7;
take p ; :: thesis: ( p . 1 = X . 1 & ( for i being non zero Nat st i < m holds
p . (i + 1) = [:(p . i),(X . (i + 1)):] ) )
thus ( p . 1 = X . 1 & ( for i being non zero Nat st i < m holds
p . (i + 1) = [:(p . i),(X . (i + 1)):] ) ) by A2, NAT_1:14; :: thesis: verum