let A be non empty set ; :: thesis: for s being stack of (StandardStackSystem A) holds |.s.| = s
defpred S1[ stack of (StandardStackSystem A)] means |.$1.| = $1;
A1: now :: thesis: for s being stack of (StandardStackSystem A) st emp s holds
S1[s]
let s be stack of (StandardStackSystem A); :: thesis: ( emp s implies S1[s] )
assume emp s ; :: thesis: S1[s]
then ( s = {} & |.s.| = {} ) by Def7, Th5;
hence S1[s] ; :: thesis: verum
end;
A2: now :: thesis: for s being stack of (StandardStackSystem A)
for e being Element of (StandardStackSystem A) st S1[s] holds
S1[ push (e,s)]
let s be stack of (StandardStackSystem A); :: thesis: for e being Element of (StandardStackSystem A) st S1[s] holds
S1[ push (e,s)]
let e be Element of (StandardStackSystem A); :: thesis: ( S1[s] implies S1[ push (e,s)] )
assume S1[s] ; :: thesis: S1[ push (e,s)]
then |.(push (e,s)).| = <*e*> ^ s by Th8;
hence S1[ push (e,s)] by Def7; :: thesis: verum
end;
let s be stack of (StandardStackSystem A); :: thesis: |.s.| = s
thus S1[s] from STACKS_1:sch 3(A1, A2); :: thesis: verum