defpred S1[ Nat] means ex S being non empty ManySortedSign st
( S = F3() . $1 & P1[S,F4() . $1,$1] );
A4:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
given S being non
empty ManySortedSign such that A5:
S = F3()
. n
and A6:
P1[
S,
F4()
. n,
n]
;
S1[n + 1]
take
F1(
S,
(F4() . n),
n)
;
( F1(S,(F4() . n),n) = F3() . (n + 1) & P1[F1(S,(F4() . n),n),F4() . (n + 1),n + 1] )
F4()
. (n + 1) = F2(
(F4() . n),
n)
by A2, A5;
hence
(
F1(
S,
(F4() . n),
n)
= F3()
. (n + 1) &
P1[
F1(
S,
(F4() . n),
n),
F4()
. (n + 1),
n + 1] )
by A2, A3, A5, A6;
verum
end;
A7:
S1[ 0 ]
by A1;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A4); verum