let X1, X2 be non empty non void strict StackSystem ; :: thesis:
assume that
A1: the carrier of X1 = A and
B1: the carrier' of X1 = A * and
C1: 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
A2: the carrier of X2 = A and
B2: the carrier' of X2 = A * and
C2: 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 A1;
reconsider e2 = x as Element of X2 by A2;
let y be Element of A * ; :: thesis:
reconsider s1 = y as stack of X1 by B1;
reconsider s2 = y as stack of X2 by B2;
thus the s_push of X1 . (x,y) = push (e1,s1)
.= <*x*> ^ y by C1
.= push (e2,s2) by C2
.= the s_push of X2 . (x,y) ; :: thesis:

end;

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

then not s1 is empty by C1;
then D2: not emp s2 by C2;
thus the s_pop of X1 . x = pop s1
.= Del (x,1) by D1, C1
.= pop s2 by D2, C2
.= the s_pop of X2 . x ; :: thesis:

end;

then s1 is empty by C1;
then D2: emp s2 by C2;
thus the s_pop of X1 . x = pop s1
.= {} by D1, C1
.= pop s2 by D2, C2
.= the s_pop of X2 . x ; :: thesis:

end;

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

then not s1 is empty by C1;
then D2: not emp s2 by C2;
thus the s_top of X1 . x = top s1
.= x . 1 by D1, C1
.= top s2 by D2, C2
.= the s_top of X2 . x ; :: thesis:

end;

then s1 is empty by C1;
then D2: emp s2 by C2;
thus the s_top of X1 . x = top s1
.= the Element of A by A1, D1, C1
.= top s2 by A2, D2, C2
.= the s_top of X2 . x ; :: thesis:

end;

the s_empty of X1 = the s_empty of X2

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in the s_empty of X1 ; :: thesis:
then reconsider s1 = x as stack of X1 ;
reconsider s2 = s1 as stack of X2 by B1, B2;
emp s1 by A6, EMP;
then s1 is empty by C1;
then emp s2 by C2;
hence x in the s_empty of X2 by EMP; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in the s_empty of X2 ; :: thesis:
then reconsider s2 = x as stack of X2 ;
reconsider s1 = s2 as stack of X1 by B1, B2;
emp s2 by A6, EMP;
then s2 is empty by C2;
then emp s1 by C1;
hence x in the s_empty of X1 by EMP; :: thesis:

end;