let X be StackAlgebra; :: thesis: 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; :: thesis: for S being stack of (X /==) st S = Class ((==_ X),s) holds
|.S.| = |.s.|
defpred S₁[ 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
S₁[s1]

proof

let s1 be stack of X; :: thesis: ( emp s1 implies S₁[s1] )
assume A2: emp s1 ; :: thesis: S₁[s1]
let S be stack of (X /==); :: thesis: ( S = Class ((==_ X),s1) implies |.S.| = |.s1.| )
assume S = Class ((==_ X),s1) ; :: thesis: |.S.| = |.s1.|
then emp S by A2, Th36;
then |.S.| = {} by Th5;
hence |.S.| = |.s1.| by A2, Th5; :: thesis: verum

end;

A3: for s1 being stack of X
for e being Element of X st S₁[s1] holds
S₁[ push (e,s1)]

proof

let s1 be stack of X; :: thesis: for e being Element of X st S₁[s1] holds
S₁[ push (e,s1)]
let e be Element of X; :: thesis: ( S₁[s1] implies S₁[ push (e,s1)] )
assume A4: S₁[s1] ; :: thesis: S₁[ push (e,s1)]
reconsider E = e as Element of (X /==) by Def20;
let S be stack of (X /==); :: thesis: ( S = Class ((==_ X),(push (e,s1))) implies |.S.| = |.(push (e,s1)).| )
assume A5: S = Class ((==_ X),(push (e,s1))) ; :: thesis: |.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 ;
:: thesis: verum

end;

thus S₁[s] from STACKS_1:sch 3(A1, A3); :: thesis: verum