let X be StackAlgebra; :: thesis: for s being stack of X
for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s )
let s be stack of X; :: thesis: for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s )
set A = the carrier of X;
defpred S₁[ FinSequence of the carrier of X] means ex s1 being stack of X st
( |.s1.| = $1 & s1 in coset s );
emp core s by Def19;
then |.(core s).| = {} by Th5;
then A1: S₁[ <*> the carrier of X] by Th29;

A2: now :: thesis: for p being FinSequence of the carrier of X
for x being Element of the carrier of X st S₁[p] holds
S₁[<*x*> ^ p]

let p be FinSequence of the carrier of X; :: thesis: for x being Element of the carrier of X st S₁[p] holds
S₁[<*x*> ^ p]
let x be Element of the carrier of X; :: thesis: ( S₁[p] implies S₁[<*x*> ^ p] )
assume S₁[p] ; :: thesis: S₁[<*x*> ^ p]
then consider s1 being stack of X such that
A3: ( |.s1.| = p & s1 in coset s ) ;
thus S₁[<*x*> ^ p] :: thesis: verum

proof

take s2 = push (x,s1); :: thesis: ( |.s2.| = <*x*> ^ p & s2 in coset s )
thus ( |.s2.| = <*x*> ^ p & s2 in coset s ) by A3, Th8, Def17; :: thesis: verum

end;

end;

for p being FinSequence of the carrier of X holds S₁[p] from STACKS_1:sch 1(A1, A2);
hence for x being Element of the carrier of X * ex s1 being stack of X st
( |.s1.| = x & s1 in coset s ) ; :: thesis: verum