defpred S₁[ Element of NAT , set , set ] means ex f being Function st
( f = p . $1 & $3 = f . $2 );
A1: for i being Element of NAT st 1 <= i & i < (len p) + 1 holds
for x being set ex y being set st S₁[i,x,y]

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < (len p) + 1 implies for x being set ex y being set st S₁[i,x,y] )
assume 1 <= i ; :: thesis: ( not i < (len p) + 1 or for x being set ex y being set st S₁[i,x,y] )
assume i < (len p) + 1 ; :: thesis: for x being set ex y being set st S₁[i,x,y]
reconsider f = p . i as Function ;
let x be set ; :: thesis: ex y being set st S₁[i,x,y]
take f . x ; :: thesis: S₁[i,x,f . x]
take f ; :: thesis: ( f = p . i & f . x = f . x )
thus ( f = p . i & f . x = f . x ) ; :: thesis: verum

end;

consider q being FinSequence such that
A3: len q = (len p) + 1 and
A4: ( q . 1 = x or (len p) + 1 = 0 ) and
A5: for i being Element of NAT st 1 <= i & i < (len p) + 1 holds
S₁[i,q . i,q . (i + 1)] from RECDEF_1:sch 3(A1);
take q ; :: thesis: ( len q = (len p) + 1 & q . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
q . (i + 1) = f . (q . i) ) )
thus ( len q = (len p) + 1 & q . 1 = x ) by A3, A4; :: thesis: for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
q . (i + 1) = f . (q . i)
let i be Element of NAT ; :: thesis: for f being Function st i in dom p & f = p . i holds
q . (i + 1) = f . (q . i)
let f be Function; :: thesis: ( i in dom p & f = p . i implies q . (i + 1) = f . (q . i) )
assume i in dom p ; :: thesis: ( not f = p . i or q . (i + 1) = f . (q . i) )
then ( i >= 1 & i <= len p ) by FINSEQ_3:27;
then ( i >= 1 & i < (len p) + 1 ) by NAT_1:13;
then ex f being Function st
( f = p . i & q . (i + 1) = f . (q . i) ) by A5;
hence ( not f = p . i or q . (i + 1) = f . (q . i) ) ; :: thesis: verum