let X be StackAlgebra; for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) holds
|.S.| = |.s.|
let s be stack of X; for S being stack of (X /==) st S = Class ((==_ X),s) holds
|.S.| = |.s.|
defpred S1[ stack of X] means for S being stack of (X /==) st S = Class ((==_ X),$1) holds
|.S.| = |.$1.|;
A1:
for s1 being stack of X st emp s1 holds
S1[s1]
A3:
for s1 being stack of X
for e being Element of X st S1[s1] holds
S1[ push (e,s1)]
proof
let s1 be
stack of
X;
for e being Element of X st S1[s1] holds
S1[ push (e,s1)]let e be
Element of
X;
( S1[s1] implies S1[ push (e,s1)] )
assume A4:
S1[
s1]
;
S1[ push (e,s1)]
reconsider E =
e as
Element of
(X /==) by Def20;
let S be
stack of
(X /==);
( S = Class ((==_ X),(push (e,s1))) implies |.S.| = |.(push (e,s1)).| )
assume A5:
S = Class (
(==_ X),
(push (e,s1)))
;
|.S.| = |.(push (e,s1)).|
reconsider P =
Class (
(==_ X),
s1) as
stack of
(X /==) by Th35;
S = push (
E,
P)
by A5, Th38;
hence |.S.| =
<*E*> ^ |.P.|
by Th8
.=
<*e*> ^ |.s1.|
by A4
.=
|.(push (e,s1)).|
by Th8
;
verum
end;
thus
S1[s]
from STACKS_1:sch 3(A1, A3); verum