let X1, X2 be StackAlgebra; for F, G being Function st F,G form_isomorphism_between X1,X2 holds
for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
let F, G be Function; ( F,G form_isomorphism_between X1,X2 implies for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.| )
assume that
A1:
( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one )
and
A2:
( dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one )
and
A3:
for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = F . (top s1) ) ) & ( for e1 being Element of X1
for e2 being Element of X2 st e2 = F . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
; STACKS_1:def 21 for s1 being stack of X1
for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
reconsider F1 = F as Function of the carrier of X1, the carrier of X2 by A1, FUNCT_2:2;
reconsider G1 = G as Function of the carrier' of X1, the carrier' of X2 by A2, FUNCT_2:2;
let s1 be stack of X1; for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
defpred S1[ stack of X1] means for s2 being stack of X2 st s2 = G . $1 holds
|.s2.| = F * |.$1.|;
A4:
for s1 being stack of X1 st emp s1 holds
S1[s1]
A6:
for s1 being stack of X1
for e being Element of X1 st S1[s1] holds
S1[ push (e,s1)]
proof
let s1 be
stack of
X1;
for e being Element of X1 st S1[s1] holds
S1[ push (e,s1)]let e be
Element of
X1;
( S1[s1] implies S1[ push (e,s1)] )
assume A7:
S1[
s1]
;
S1[ push (e,s1)]
let s2 be
stack of
X2;
( s2 = G . (push (e,s1)) implies |.s2.| = F * |.(push (e,s1)).| )
A8:
|.(G1 . s1).| = F * |.s1.|
by A7;
A9:
<*(F1 . e)*> = F * <*e*>
by A1, FINSEQ_2:34;
assume
s2 = G . (push (e,s1))
;
|.s2.| = F * |.(push (e,s1)).|
then
s2 = push (
(F1 . e),
(G1 . s1))
by A3;
hence |.s2.| =
<*(F1 . e)*> ^ |.(G1 . s1).|
by Th8
.=
F * (<*e*> ^ |.s1.|)
by A8, A9, FINSEQOP:9
.=
F * |.(push (e,s1)).|
by Th8
;
verum
end;
thus
S1[s1]
from STACKS_1:sch 3(A4, A6); verum