let X1, X2 be non empty non void strict StackSystem ; :: thesis: ( the carrier of X1 = A & the carrier' of X1 = A * & ( for s being stack of X1 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 X1 & pop s = {} ) ) & ( for e being Element of X1 holds push (e,s) = <*e*> ^ g ) ) ) ) ) & the carrier of X2 = A & the carrier' of X2 = A * & ( for s being stack of X2 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 X2 & pop s = {} ) ) & ( for e being Element of X2 holds push (e,s) = <*e*> ^ g ) ) ) ) ) implies X1 = X2 )
assume that
A9: the carrier of X1 = A and
A10: the carrier' of X1 = A * and
A11: for s being stack of X1 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 X1 & pop s = {} ) ) & ( for e being Element of X1 holds push (e,s) = <*e*> ^ g ) ) ) ) and
A12: the carrier of X2 = A and
A13: the carrier' of X2 = A * and
A14: for s being stack of X2 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 X2 & pop s = {} ) ) & ( for e being Element of X2 holds push (e,s) = <*e*> ^ g ) ) ) ) ; :: thesis: X1 = X2

now :: thesis: for x being Element of A
for y being Element of A * holds the s_push of X1 . (x,y) = the s_push of X2 . (x,y)

let x be Element of A; :: thesis: for y being Element of A * holds the s_push of X1 . (x,y) = the s_push of X2 . (x,y)
reconsider e1 = x as Element of X1 by A9;
reconsider e2 = x as Element of X2 by A12;
let y be Element of A * ; :: thesis: the s_push of X1 . (x,y) = the s_push of X2 . (x,y)
reconsider s1 = y as stack of X1 by A10;
reconsider s2 = y as stack of X2 by A13;
thus the s_push of X1 . (x,y) = push (e1,s1)
.= <*x*> ^ y by A11
.= push (e2,s2) by A14
.= the s_push of X2 . (x,y) ; :: thesis: verum

end;

then A15: the s_push of X1 = the s_push of X2 by A9, A10, A12, A13, BINOP_1:2;

now :: thesis: for x being Element of A * holds the s_pop of X1 . x = the s_pop of X2 . x

let x be Element of A * ; :: thesis: the s_pop of X1 . b₁ = the s_pop of X2 . b₁
reconsider s1 = x as stack of X1 by A10;
reconsider s2 = x as stack of X2 by A13;

per cases ( not emp s1 or emp s1 ) ;

suppose A16: not emp s1 ; :: thesis: the s_pop of X1 . b₁ = the s_pop of X2 . b₁

then not s1 is empty by A11;
then A17: not emp s2 by A14;
thus the s_pop of X1 . x = pop s1
.= Del (x,1) by A16, A11
.= pop s2 by A17, A14
.= the s_pop of X2 . x ; :: thesis: verum

end;

suppose A18: emp s1 ; :: thesis: the s_pop of X1 . b₁ = the s_pop of X2 . b₁

then s1 is empty by A11;
then A19: emp s2 by A14;
thus the s_pop of X1 . x = pop s1
.= {} by A18, A11
.= pop s2 by A19, A14
.= the s_pop of X2 . x ; :: thesis: verum

end;

end;

end;

then A20: the s_pop of X1 = the s_pop of X2 by A10, A13;

A21: now :: thesis: for x being Element of A * holds the s_top of X1 . x = the s_top of X2 . x

let x be Element of A * ; :: thesis: the s_top of X1 . b₁ = the s_top of X2 . b₁
reconsider s1 = x as stack of X1 by A10;
reconsider s2 = x as stack of X2 by A13;

per cases ( not emp s1 or emp s1 ) ;

suppose A22: not emp s1 ; :: thesis: the s_top of X1 . b₁ = the s_top of X2 . b₁

then not s1 is empty by A11;
then A23: not emp s2 by A14;
thus the s_top of X1 . x = top s1
.= x . 1 by A22, A11
.= top s2 by A23, A14
.= the s_top of X2 . x ; :: thesis: verum

end;

suppose A24: emp s1 ; :: thesis: the s_top of X1 . b₁ = the s_top of X2 . b₁

then s1 is empty by A11;
then A25: emp s2 by A14;
thus the s_top of X1 . x = top s1
.= the Element of A by A9, A24, A11
.= top s2 by A12, A25, A14
.= the s_top of X2 . x ; :: thesis: verum

end;

end;

end;

the s_empty of X1 = the s_empty of X2

proof

thus the s_empty of X1 c= the s_empty of X2 :: according to XBOOLE_0:def 10 :: thesis: the s_empty of X2 c= the s_empty of X1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the s_empty of X1 or x in the s_empty of X2 )
assume A26: x in the s_empty of X1 ; :: thesis: x in the s_empty of X2
then reconsider s1 = x as stack of X1 ;
reconsider s2 = s1 as stack of X2 by A10, A13;
emp s1 by A26;
then s1 is empty by A11;
then emp s2 by A14;
hence x in the s_empty of X2 ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the s_empty of X2 or x in the s_empty of X1 )
assume A27: x in the s_empty of X2 ; :: thesis: x in the s_empty of X1
then reconsider s2 = x as stack of X2 ;
reconsider s1 = s2 as stack of X1 by A10, A13;
emp s2 by A27;
then s2 is empty by A14;
then emp s1 by A11;
hence x in the s_empty of X1 ; :: thesis: verum

end;

hence X1 = X2 by A9, A10, A12, A15, A20, A21, FUNCT_2:63; :: thesis: verum