let X be StackAlgebra; for s being stack of X ex s1 being stack of X st
( emp s1 & s1 in coset s )
let s be stack of X; ex s1 being stack of X st
( emp s1 & s1 in coset s )
deffunc H1( stack of X) -> stack of X = pop $1;
defpred S1[ set , stack of X, set ] means $3 = IFIN ($2, the s_empty of X,s,(pop $2));
A1:
for n being Nat
for x being stack of X ex y being stack of X st S1[n,x,y]
;
consider f being sequence of the carrier' of X such that
A2:
( f . 0 = s & ( for i being Nat holds S1[i,f . i,f . (i + 1)] ) )
from RECDEF_1:sch 2(A1);
defpred S2[ Nat] means f . $1 in coset s;
A3:
S2[ 0 ]
by A2, Def17;
A4:
now for i being Nat st S2[i] holds
S2[i + 1]end;
A6:
for i being Nat holds S2[i]
from NAT_1:sch 2(A3, A4);
consider i being Nat, s1 being stack of X such that
A7:
( f . i = s1 & ( not emp s1 implies f . (i + 1) <> pop s1 ) )
by Def8;
take
s1
; ( emp s1 & s1 in coset s )
f . (i + 1) = IFIN ((f . i), the s_empty of X,s,(pop (f . i)))
by A2;
then
( ( f . i in the s_empty of X implies f . (i + 1) = s ) & ( f . i nin the s_empty of X implies f . (i + 1) = pop (f . i) ) )
by MATRIX_7:def 1;
hence
( emp s1 & s1 in coset s )
by A7, A6; verum