consider p being FinSequence of F₁() such that
A2: len p = F₃() and
A3: ( p . 1 = F₂() or F₃() = 0 ) and
A4: for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p . n,p . (n + 1)] from RECDEF_1:sch 4(A1);
take p ; :: thesis: ( len p = F₃() & ( p /. 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p /. n,p /. (n + 1)] ) )
thus len p = F₃() by A2; :: thesis: ( ( p /. 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p /. n,p /. (n + 1)] ) )

now :: thesis: ( F₃() <> 0 implies p /. 1 = F₂() )

assume F₃() <> 0 ; :: thesis: p /. 1 = F₂()
then F₃() >= 0 + 1 by NAT_1:13;
hence p /. 1 = F₂() by A2, A3, FINSEQ_4:15; :: thesis: verum

end;

hence ( p /. 1 = F₂() or F₃() = 0 ) ; :: thesis: for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p /. n,p /. (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < F₃() implies P₁[n,p /. n,p /. (n + 1)] )
assume that
A5: 1 <= n and
A6: n < F₃() ; :: thesis: P₁[n,p /. n,p /. (n + 1)]
n + 1 <= F₃() by A6, NAT_1:13;
then A7: p . (n + 1) = p /. (n + 1) by A2, FINSEQ_4:15, NAT_1:11;
( n in NAT & p . n = p /. n ) by A2, A5, A6, FINSEQ_4:15, ORDINAL1:def 12;
hence P₁[n,p /. n,p /. (n + 1)] by A4, A5, A6, A7; :: thesis: verum