consider p being FinSequence of F1() such that
A2: len p = F3() and
A3: ( p . 1 = F2() or F3() = 0 ) and
A4: for n being Nat st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] from RECDEF_1:sch 4(A1);
 take p ; :: thesis: ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)] ) )
thus len p = F3() by A2; :: thesis: ( ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)] ) )
now :: thesis: ( F3() <> 0 implies p /. 1 = F2() )
assume F3() <> 0 ; :: thesis: p /. 1 = F2()
then F3() >= 0 + 1 by NAT_1:13;
hence p /. 1 = F2() by A2, A3, FINSEQ_4:15; :: thesis: verum
end;
hence ( p /. 1 = F2() or F3() = 0 ) ; :: thesis: for n being Nat st 1 <= n & n < F3() holds
P1[n,p /. n,p /. (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < F3() implies P1[n,p /. n,p /. (n + 1)] )
assume that
A5: 1 <= n and
A6: n < F3() ; :: thesis: P1[n,p /. n,p /. (n + 1)]
n + 1 <= F3() 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 P1[n,p /. n,p /. (n + 1)] by A4, A5, A6, A7; :: thesis: verum