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