defpred S1[ set , stack of F1(), stack of F1()] means $3 = pop $2;
A1: for n being Element of NAT
for x being stack of F1() ex y being stack of F1() st S1[n,x,y] ;
consider f being Function of NAT, the carrier' of F1() such that
A2: ( f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
 consider i being Nat, s being stack of F1() such that
A3: ( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) ) by POPFIN;
defpred S2[ Nat] means P1[f . (i -' $1)];
i -' 0 = i by NAT_D:40;
then A5: S2[ 0 ] by A3, A2, P1;
A6: now
let j be Nat; :: thesis: ( S2[j] implies S2[b1 + 1] )
assume B1: S2[j] ; :: thesis: S2[b1 + 1]
B2: i -' (j + 1) = (i -' j) -' 1 by NAT_2:30;
per cases ( i -' j >= 1 or i -' j < 0 + 1 ) ;
suppose i -' j >= 1 ; :: thesis: S2[b1 + 1]
then (i -' (j + 1)) + 1 = i -' j by B2, XREAL_1:235;
then f . (i -' j) = pop (f . (i -' (j + 1))) by A2;
then ( not emp f . (i -' (j + 1)) implies f . (i -' (j + 1)) = push ((top (f . (i -' (j + 1)))),(f . (i -' j))) ) by PUSHPOP;
hence S2[j + 1] by P1, P2, B1; :: thesis: verum
end;
suppose B7: i -' j < 0 + 1 ; :: thesis: S2[b1 + 1]
then B6: i -' j <= 0 by NAT_1:13;
B4: i -' j = 0 by B7, NAT_1:13;
i -' (j + 1) = 0 -' 1 by B4, NAT_2:30
.= 0 by NAT_2:8 ;
hence S2[j + 1] by B1, B6; :: thesis: verum
end;
end;
end;
for j being Nat holds S2[j] from NAT_1:sch 2(A5, A6);
 then S2[i] ;
hence P1[F2()] by A2, XREAL_1:232; :: thesis: verum