defpred S1[ set , stack of F1(), stack of F1()] means $3 = pop $2;
A3:
for n being Nat
for x being stack of F1() ex y being stack of F1() st S1[n,x,y]
;
consider f being sequence of the carrier' of F1() such that
A4:
( f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A3);
consider i being Nat, s being stack of F1() such that
A5:
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
by Def8;
defpred S2[ Nat] means P1[f . (i -' $1)];
i -' 0 = i
by NAT_D:40;
then A6:
S2[ 0 ]
by A5, A4, A1;
A7:
now for j being Nat st S2[j] holds
S2[j + 1]let j be
Nat;
( S2[j] implies S2[b1 + 1] )assume A8:
S2[
j]
;
S2[b1 + 1]A9:
i -' (j + 1) = (i -' j) -' 1
by NAT_2:30;
end;
for j being Nat holds S2[j]
from NAT_1:sch 2(A6, A7);
then
S2[i]
;
hence
P1[F2()]
by A4, XREAL_1:232; verum