let X be StackAlgebra; :: thesis: for s1, s, s2 being stack of X st s1 in coset s & s2 in coset s & |.s1.| = |.s2.| holds
s1 = s2
let s1, s, s2 be stack of X; :: thesis: ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2 )
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]

proof

let s1 be stack of X; :: thesis: ( emp s1 implies S₁[s1] )
assume AA: emp s1 ; :: thesis: S₁[s1]
then A2: |.s1.| = {} by Th31;
let s2 be stack of X; :: thesis: ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2 )
assume ( s1 in coset s & s2 in coset s & |.s1.| = |.s2.| ) ; :: thesis: s1 = s2
then ( core s1 = core s & core s2 = core s & emp s2 ) by A2, Th351, Th14;
then ( core s = s1 & core s = s2 ) by AA, Th11;
hence s1 = s2 ; :: thesis: verum

end;

A4: now

let s1 be stack of X; :: thesis: for e being Element of X st S₁[s1] holds
S₁[ push (e,s1)]
let e be Element of X; :: thesis: ( S₁[s1] implies S₁[ push (e,s1)] )
assume A5: S₁[s1] ; :: thesis: S₁[ push (e,s1)]
thus S₁[ push (e,s1)] :: thesis: verum

proof

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

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: verum