set R = ConstructionRed X;
deffunc H₁( stack of X) -> stack of X = pop $1;
defpred S₁[ 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 S₁[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 S₁[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch 2(A0);
defpred S₂[ Nat] means ex s1 being stack of X st
( f . $1 = s1 & ( not emp s1 implies f . ($1 + 1) <> pop s1 ) );
A5: ex i being Nat st S₂[i] by POPFIN;
consider i being Nat such that
A6: ( S₂[i] & ( for j being Nat st S₂[j] holds
i <= j ) ) from NAT_1:sch 5(A5);
deffunc H₂( Nat) -> Element of the carrier' of X = f . ($1 -' 1);
consider t being FinSequence such that
A7: ( len t = i + 1 & ( for j being Nat st j in dom t holds
t . j = H₂(j) ) ) from FINSEQ_1:sch 2();
consider s1 being stack of X such that
A8: ( f . i = s1 & ( not emp s1 implies f . (i + 1) <> pop s1 ) ) by A6;
take s1 ; :: thesis:
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 by A8, EMP; :: thesis:
A9: t is RedSequence of ConstructionRed X

thus len t > 0 by A7; :: according to REWRITE1:def 2 :: thesis:
let j be Element of NAT ; :: thesis:
assume B1: ( j in dom t & j + 1 in dom t ) ; :: thesis:
then ( j >= 1 & j <= i + 1 & j + 1 <= i + 1 ) by A7, FINSEQ_3:25;
then B2: ( (j -' 1) + 1 = j & (j + 1) -' 1 = j & j <= i ) by NAT_D:34, XREAL_1:6, XREAL_1:235;
j -' 1 < i by B2, NAT_1:13;
then B7: not emp f . (j -' 1) by A6;
then B4: f . (j -' 1) nin the s_empty of X by EMP;
B5: ( t . j = f . (j -' 1) & t . (j + 1) = f . j ) by A7, B1, B2;
then S₁[j -' 1,f . (j -' 1),t . (j + 1)] by A1, B2;
then t . (j + 1) = pop (f . (j -' 1)) by B4, MATRIX_7:def 1;
hence [(t . j),(t . (j + 1))] in ConstructionRed X by B5, B7, CRED; :: thesis:

end;

then 1 in dom t by FINSEQ_5:6;
then C1: t . 1 = f . (1 -' 1) by A7
.= s by A1, XREAL_1:232 ;
then reconsider t = t as the carrier' of X -valued RedSequence of ConstructionRed X by A9, Lem2;
take t ; :: thesis:
thus t . 1 = s by C1; :: thesis:
len t in dom t by FINSEQ_5:6;
hence t . (len t) = f . ((i + 1) -' 1) by A7
.= s1 by A8, NAT_D:34 ;
:: thesis:
let k be Nat; :: thesis:
assume C2: ( 1 <= k & k < len t ) ; :: thesis:
then k in dom t by FINSEQ_3:25;
then C3: ( t . k = f . (k -' 1) & t . k = t /. k ) by A7, PARTFUN1:def 6;
( 1 <= k + 1 & k + 1 <= len t ) by C2, NAT_1:13;
then k + 1 in dom t by FINSEQ_3:25;
then C4: ( t . (k + 1) = f . ((k + 1) -' 1) & t . (k + 1) = t /. (k + 1) ) by A7, PARTFUN1:def 6;
C6: ( (k -' 1) + 1 = k & (k + 1) -' 1 = k ) by C2, NAT_D:34, XREAL_1:235;
then k -' 1 < i by A7, C2, XREAL_1:6;
hence not emp t /. k by A6, C3; :: thesis:
then C5: t /. k nin the s_empty of X by EMP;
f . k = IFIN ((f . (k -' 1)), the s_empty of X,s,(pop (f . (k -' 1)))) by A1, C6;
hence t /. (k + 1) = pop (t /. k) by C3, C4, C6, C5, MATRIX_7:def 1; :: thesis: