let X1, X2 be StackAlgebra; :: thesis: 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; :: thesis: ( 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)) ) ) ; :: according to STACKS_1:def 21 :: thesis: 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; :: thesis: for s2 being stack of X2 st s2 = G . s1 holds
|.s2.| = F * |.s1.|
defpred S₁[ 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
S₁[s1]

proof

let s1 be stack of X1; :: thesis: ( emp s1 implies S₁[s1] )
assume A5: emp s1 ; :: thesis: S₁[s1]
let s2 be stack of X2; :: thesis: ( s2 = G . s1 implies |.s2.| = F * |.s1.| )
assume s2 = G . s1 ; :: thesis: |.s2.| = F * |.s1.|
then emp s2 by A3, A5;
then ( |.s2.| = {} & |.s1.| = {} ) by A5, Th5;
hence |.s2.| = F * |.s1.| ; :: thesis: verum

end;

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

proof

let s1 be stack of X1; :: thesis: for e being Element of X1 st S₁[s1] holds
S₁[ push (e,s1)]
let e be Element of X1; :: thesis: ( S₁[s1] implies S₁[ push (e,s1)] )
assume A7: S₁[s1] ; :: thesis: S₁[ push (e,s1)]
let s2 be stack of X2; :: thesis: ( 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)) ; :: thesis: |.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 ;
:: thesis: verum

end;

thus S₁[s1] from STACKS_1:sch 3(A4, A6); :: thesis: verum