let X1, X2 be non empty non void strict StackSystem ; :: thesis:
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:

let x be Element of A; :: thesis:
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:
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:

end;

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

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:

end;

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:

end;

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

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:

end;

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:

end;

the s_empty of X1 = the s_empty of X2

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: x in the s_empty of X1 ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in the s_empty of X2 ; :: thesis:
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:

end;