set X = StandardStackSystem A;
let f be sequence of the carrier' of (StandardStackSystem A); :: according to STACKS_1:def 8 :: thesis: ex i being Nat ex s being stack of (StandardStackSystem A) st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
assume A1: for i being Nat
for s being stack of (StandardStackSystem A) st f . i = s holds
( not emp s & f . (i + 1) = pop s ) ; :: thesis: contradiction
reconsider g = f . 1 as Element of A * by Def7;
defpred S₁[ Nat] means ex i being Nat ex g being Element of A * st
( g = f . i & A = len g );
A2: ex k being Nat st S₁[k]

proof

take k = len g; :: thesis: S₁[k]
take i = 1; :: thesis: ex g being Element of A * st
( g = f . i & k = len g )
take g ; :: thesis: ( g = f . i & k = len g )
thus ( g = f . i & k = len g ) ; :: thesis: verum

end;

A3: for k being Nat st k <> 0 & S₁[k] holds
ex n being Nat st
( n < k & S₁[n] )

proof

let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex n being Nat st
( n < k & S₁[n] ) )
assume A4: k <> 0 ; :: thesis: ( not S₁[k] or ex n being Nat st
( n < k & S₁[n] ) )
then consider n0 being Nat such that
A5: k = n0 + 1 by NAT_1:6;
given i being Nat, g being Element of A * such that A6: ( g = f . i & k = len g ) ; :: thesis: ex n being Nat st
( n < k & S₁[n] )
reconsider s = g as stack of (StandardStackSystem A) by A6;
reconsider h = pop s as Element of A * by Def7;
take n = len h; :: thesis: ( n < k & S₁[n] )
A7: not s is empty by A4, A6;
then not emp s by Def7;
then A8: ( f . (i + 1) = pop s & h = Del (g,1) ) by A1, A6, Def7;
1 in dom g by A7, FINSEQ_5:6;
then n0 = n by A5, A6, A8, FINSEQ_3:109;
hence ( n < k & S₁[n] ) by A5, A8, NAT_1:13; :: thesis: verum

end;

S₁[ 0 ] from NAT_1:sch 7(A2, A3);
then consider i being Nat, g being Element of A * such that
A9: ( g = f . i & 0 = len g ) ;
reconsider s = g as stack of (StandardStackSystem A) by A9;
( g is empty & not emp s ) by A1, A9;
hence contradiction by Def7; :: thesis: verum