set X = StandardStackSystem A;
let f be Function of NAT, 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 E1: 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 EXAM;
defpred S₁[ Nat] means ex i being Nat ex g being Element of A * st
( g = f . i & A = len g );
E2: 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;

E3: 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 E4: k <> 0 ; :: thesis: ( not S₁[k] or ex n being Nat st
( n < k & S₁[n] ) )
then consider n0 being Nat such that
E7: k = n0 + 1 by NAT_1:6;
given i being Nat, g being Element of A * such that E5: ( 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 E5;
reconsider h = pop s as Element of A * by EXAM;
take n = len h; :: thesis: ( n < k & S₁[n] )
E8: not s is empty by E4, E5;
then not emp s by EXAM;
then E6: ( f . (i + 1) = pop s & h = Del (g,1) ) by E1, E5, EXAM;
1 in dom g by E8, FINSEQ_5:6;
then n0 = n by E7, E5, E6, FINSEQ_3:109;
hence ( n < k & S₁[n] ) by E7, E6, NAT_1:13; :: thesis: verum

end;

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