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 :: thesis: for j being Nat st S2[j] holds
S2[j + 1]
let j be Nat; :: thesis: ( S2[j] implies S2[b1 + 1] )
assume A8: S2[j] ; :: thesis: S2[b1 + 1]
A9: 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 A9, XREAL_1:235;
then f . (i -' j) = pop (f . (i -' (j + 1))) by A4;
then ( not emp f . (i -' (j + 1)) implies f . (i -' (j + 1)) = push ((top (f . (i -' (j + 1)))),(f . (i -' j))) ) by Def9;
hence S2[j + 1] by A1, A2, A8; :: thesis: verum
end;
suppose A10: i -' j < 0 + 1 ; :: thesis: S2[b1 + 1]
then A11: i -' j <= 0 by NAT_1:13;
A12: i -' j = 0 by A10, NAT_1:13;
i -' (j + 1) = 0 -' 1 by A12, NAT_2:30
.= 0 by NAT_2:8 ;
hence S2[j + 1] by A8, A11; :: thesis: verum
end;
end;
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; :: thesis: verum