defpred S₁[ Nat, set , set ] means ex f being Function st
( f = p . $1 & $3 = f . $2 );
A1: for i being 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 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
A2: ( len q = (len p) + 1 & ( q . 1 = x or (len p) + 1 = 0 ) ) and
A3: for i being 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 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 A2; :: thesis: for i being Nat
for f being Function st i in dom p & f = p . i holds
q . (i + 1) = f . (q . i)
let i be 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 A4: i in dom p ; :: thesis: ( not f = p . i or q . (i + 1) = f . (q . i) )
then i <= len p by FINSEQ_3:25;
then A5: i < (len p) + 1 by NAT_1:13;
i >= 1 by A4, FINSEQ_3:25;
then ex f being Function st
( f = p . i & q . (i + 1) = f . (q . i) ) by A3, A5;
hence ( not f = p . i or q . (i + 1) = f . (q . i) ) ; :: thesis: verum