let X1, X2 be strict StackSystem ; ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of (Class (==_ X)) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) & the carrier of X2 = the carrier of X & the carrier' of X2 = Class (==_ X) & the s_empty of X2 = { the s_empty of X} & the s_push of X2 = the s_push of X /\/ (==_ X) & the s_pop of X2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of (Class (==_ X)) holds the s_top of X2 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) implies X1 = X2 )
assume that
A1:
( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) )
and
A2:
for f being Choice_Function of (Class (==_ X)) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)
and
A3:
( the carrier of X2 = the carrier of X & the carrier' of X2 = Class (==_ X) & the s_empty of X2 = { the s_empty of X} & the s_push of X2 = the s_push of X /\/ (==_ X) & the s_pop of X2 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) )
and
A4:
for f being Choice_Function of (Class (==_ X)) holds the s_top of X2 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)
; X1 = X2
set f = the Choice_Function of (Class (==_ X));
( the s_top of X1 = ( the s_top of X * the Choice_Function of (Class (==_ X))) +* ( the s_empty of X, the Element of the carrier of X) & the s_top of X2 = ( the s_top of X * the Choice_Function of (Class (==_ X))) +* ( the s_empty of X, the Element of the carrier of X) )
by A2, A4;
hence
X1 = X2
by A1, A3; verum