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));
A0: for n being Element of NAT
for x being stack of X ex y being stack of X st S1[n,x,y] ;
consider f being Function of NAT, the carrier' of X such that
A1: ( f . 0 = s & ( for i being Element of NAT holds S1[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch 2(A0);
 defpred S2[ Nat] means f . $1 in coset s;
A2: S2[ 0 ] by A1, COSET;
A3: now
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume B1: S2[i] ; :: thesis: S2[i + 1]
i in NAT by ORDINAL1:def 12;
then f . (i + 1) = IFIN ((f . i), the s_empty of X,s,(pop (f . i))) by A1;
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) ) ) by EMP;
hence S2[i + 1] by B1, COSET; :: thesis: verum
end;
A4: for i being Nat holds S2[i] from NAT_1:sch 2(A2, A3);
 consider i being Nat, s1 being stack of X such that
A5: ( f . i = s1 & ( not emp s1 implies f . (i + 1) <> pop s1 ) ) by POPFIN;
take s1 ; :: thesis: ( emp s1 & s1 in coset s )
i in NAT by ORDINAL1:def 12;
then f . (i + 1) = IFIN ((f . i), the s_empty of X,s,(pop (f . i))) by A1;
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 A5, A4, EMP; :: thesis: verum