let X be StackAlgebra; :: thesis: for x being Element of the carrier of X * ex s being stack of X st |.s.| = x
set D = the carrier of X;
defpred S1[ FinSequence of the carrier of X] means ex s being stack of X st |.s.| = $1;
A1: S1[ <*> the carrier of X]
proof
consider s being stack of X such that
A2: emp s by Th2;
take s ; :: thesis: |.s.| = <*> the carrier of X
thus |.s.| = <*> the carrier of X by A2, Th5; :: thesis: verum
end;
A3: 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]
proof
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] )
given s being stack of X such that A4: |.s.| = p ; :: thesis: S1[<*x*> ^ p]
take s2 = push (x,s); :: thesis: |.s2.| = <*x*> ^ p
thus |.s2.| = <*x*> ^ p by A4, Th8; :: thesis: verum
end;
for p being FinSequence of the carrier of X holds S1[p] from STACKS_1:sch 1(A1, A3);
 hence for x being Element of the carrier of X * ex s being stack of X st |.s.| = x ; :: thesis: verum