let X be StackAlgebra; :: thesis: 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; :: thesis: 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 :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A5: S2[i] ; :: thesis: S2[i + 1]
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;
then ( f . (i + 1) = s or ( not emp f . i & f . (i + 1) = pop (f . i) ) ) ;
hence S2[i + 1] by A5, Def17; :: thesis: verum
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 ; :: thesis: ( 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; :: thesis: verum