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));
A1: for n being Nat
for x being stack of X ex y being stack of X st S₁[n,x,y] ;
consider f being sequence of the carrier' of X such that
A2: ( f . 0 = s & ( for i being Nat holds S₁[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch 2(A1);
defpred S₂[ Nat] means ex s1 being stack of X st
( f . $1 = s1 & ( not emp s1 implies f . ($1 + 1) <> pop s1 ) );
A3: ex i being Nat st S₂[i] by Def8;
consider i being Nat such that
A4: ( S₂[i] & ( for j being Nat st S₂[j] holds
i <= j ) ) from NAT_1:sch 5(A3);
deffunc H₂( Nat) -> Element of the carrier' of X = f . ($1 -' 1);
consider t being FinSequence such that
A5: ( 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
A6: ( f . i = s1 & ( not emp s1 implies f . (i + 1) <> pop s1 ) ) by A4;
take s1 ; :: thesis:
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 by A6; :: thesis:
A7: t is RedSequence of ConstructionRed X

thus len t > 0 by A5; :: according to REWRITE1:def 2 :: thesis:
let j be Nat; :: thesis:
assume A8: ( j in dom t & j + 1 in dom t ) ; :: thesis:
then ( j >= 1 & j <= i + 1 & j + 1 <= i + 1 ) by A5, FINSEQ_3:25;
then A9: ( (j -' 1) + 1 = j & (j + 1) -' 1 = j & j <= i ) by NAT_D:34, XREAL_1:6, XREAL_1:235;
j -' 1 < i by A9, NAT_1:13;
then A10: not emp f . (j -' 1) by A4;
then A11: f . (j -' 1) nin the s_empty of X ;
A12: ( t . j = f . (j -' 1) & t . (j + 1) = f . j ) by A5, A8, A9;
then S₁[j -' 1,f . (j -' 1),t . (j + 1)] by A2, A9;
then t . (j + 1) = pop (f . (j -' 1)) by A11, MATRIX_7:def 1;
hence [(t . j),(t . (j + 1))] in ConstructionRed X by A12, A10, Def18; :: thesis:

end;

then 1 in dom t by FINSEQ_5:6;
then A13: t . 1 = f . (1 -' 1) by A5
.= s by A2, XREAL_1:232 ;
then reconsider t = t as the carrier' of X -valued RedSequence of ConstructionRed X by A7, Th23;
take t ; :: thesis:
thus t . 1 = s by A13; :: thesis:
len t in dom t by FINSEQ_5:6;
hence t . (len t) = f . ((i + 1) -' 1) by A5
.= s1 by A6, NAT_D:34 ;
:: thesis:
let k be Nat; :: thesis:
assume A14: ( 1 <= k & k < len t ) ; :: thesis:
then k in dom t by FINSEQ_3:25;
then A15: ( t . k = f . (k -' 1) & t . k = t /. k ) by A5, PARTFUN1:def 6;
( 1 <= k + 1 & k + 1 <= len t ) by A14, NAT_1:13;
then k + 1 in dom t by FINSEQ_3:25;
then A16: ( t . (k + 1) = f . ((k + 1) -' 1) & t . (k + 1) = t /. (k + 1) ) by A5, PARTFUN1:def 6;
A17: ( (k -' 1) + 1 = k & (k + 1) -' 1 = k ) by A14, NAT_D:34, XREAL_1:235;
then k -' 1 < i by A5, A14, XREAL_1:6;
hence not emp t /. k by A4, A15; :: thesis:
then A18: t /. k nin the s_empty of X ;
f . k = IFIN ((f . (k -' 1)), the s_empty of X,s,(pop (f . (k -' 1)))) by A2, A17;
hence t /. (k + 1) = pop (t /. k) by A15, A16, A17, A18, MATRIX_7:def 1; :: thesis: