let X be StackAlgebra; :: thesis:
let s, s1, s2 be stack of X; :: thesis:
defpred S₁[ stack of X] means for s2 being stack of X st $1 in coset s & s2 in coset s & |.$1.| = |.s2.| holds
$1 = s2;
A1: for s1 being stack of X st emp s1 holds
S₁[s1]

let s1 be stack of X; :: thesis:
assume A2: emp s1 ; :: thesis:
then A3: |.s1.| = {} by Th5;
let s2 be stack of X; :: thesis:
assume ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| ) ; :: thesis:
then ( core s1 = core s & core s2 = core s & emp s2 ) by A3, Th10, Th31;
then ( core s = s1 & core s = s2 ) by A2, Th26;
hence s1 = s2 ; :: thesis:

end;

A4: now :: thesis:

let s1 be stack of X; :: thesis:
let e be Element of X; :: thesis:
assume A5: S₁[s1] ; :: thesis:
thus S₁[ push (e,s1)] :: thesis:

let s2 be stack of X; :: thesis:
assume A6: ( push (e,s1) in coset s & s2 in coset s & |.(push (e,s1)).| = |.s2.| ) ; :: thesis:
then A7: |.s2.| = <*e*> ^ |.s1.| by Th8;
then not emp s2 by Th5;
then A8: s2 = push ((top s2),(pop s2)) by Def9;
then A9: ( s1 in coset s & pop s2 in coset s ) by A6, Th20;
|.s2.| = <*(top s2)*> ^ |.(pop s2).| by A8, Th8;
then ( e = |.s2.| . 1 & |.s2.| . 1 = top s2 & |.s1.| = |.(pop s2).| ) by A7, FINSEQ_1:41, HILBERT2:2;
hence push (e,s1) = s2 by A5, A8, A9; :: thesis:

end;

end;

S₁[s1] from STACKS_1:sch 3(A1, A4);
hence ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2 ) ; :: thesis: