reconsider s0 = <*> A as Element of A * by FINSEQ_1:def 11;
set E = {s0};
deffunc H₁( Element of A, Element of A * ) -> Element of A * = <*$1*> ^ $2;
deffunc H₂( Element of A * ) -> Element of A * = Del ($1,1);
deffunc H₃( Element of A * ) -> Element of A = IFEQ ($1,{}, the Element of A,($1 /. 1));
consider psh being Function of [:A,(A *):],(A *) such that
A1: for a being Element of A
for s being Element of A * holds psh . (a,s) = H₁(a,s) from BINOP_1:sch 4();
consider pp being Function of (A *),(A *) such that
A2: for s being Element of A * holds pp . s = H₂(s) from FUNCT_2:sch 4();
consider tp being Function of (A *),A such that
A3: for s being Element of A * holds tp . s = H₃(s) from FUNCT_2:sch 4();
take X = StackSystem(# A,(A *),{s0},psh,pp,tp #); :: thesis: ( the carrier of X = A & the carrier' of X = A * & ( for s being stack of X holds
( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) ) ) )
thus ( the carrier of X = A & the carrier' of X = A * ) ; :: thesis: for s being stack of X holds
( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) )
let s be stack of X; :: thesis: ( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) )
thus A4: ( emp s iff s is empty ) by TARSKI:def 1; :: thesis: for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
let g be FinSequence; :: thesis: ( g = s implies ( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) )
assume A5: g = s ; :: thesis: ( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
then reconsider h = g as Element of A * ;

hereby :: thesis: ( ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )

assume A6: not emp s ; :: thesis: ( top s = g . 1 & pop s = Del (g,1) )
then A7: 1 in dom h by A4, A5, FINSEQ_5:6;
thus top s = IFEQ (s,{}, the Element of A,(h /. 1)) by A3, A5
.= h /. 1 by A4, A6, FUNCOP_1:def 8
.= g . 1 by A7, PARTFUN1:def 6 ; :: thesis: pop s = Del (g,1)
thus pop s = Del (g,1) by A5, A2; :: thesis: verum

end;

hereby :: thesis: for e being Element of X holds push (e,s) = <*e*> ^ g

assume A8: emp s ; :: thesis: ( top s = the Element of X & pop s = {} )
thus top s = IFEQ (s,{}, the Element of A,(h /. 1)) by A3, A5
.= the Element of X by A4, A8, FUNCOP_1:def 8 ; :: thesis: pop s = {}
thus pop s = Del (g,1) by A5, A2
.= {} by A4, A5, A8, Th1 ; :: thesis: verum

end;

let e be Element of X; :: thesis: push (e,s) = <*e*> ^ g
thus push (e,s) = <*e*> ^ g by A1, A5; :: thesis: verum