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 S₁[ FinSequence of the carrier of X] means ex s being stack of X st |.s.| = $1;
A1: S₁[ <*> 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 S₁[p] holds
S₁[<*x*> ^ p]

proof

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] )
given s being stack of X such that A4: |.s.| = p ; :: thesis: S₁[<*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 S₁[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