let X1, X2 be StackAlgebra; for F, G being Function st F,G form_isomorphism_between X1,X2 holds
F " ,G " form_isomorphism_between X2,X1
let F, G be Function; ( F,G form_isomorphism_between X1,X2 implies F " ,G " form_isomorphism_between X2,X1 )
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 F " ,G " form_isomorphism_between X2,X1
thus
( dom (F ") = the carrier of X2 & rng (F ") = the carrier of X1 & F " is one-to-one )
by A1, FUNCT_1:33; STACKS_1:def 21 ( dom (G ") = the carrier' of X2 & rng (G ") = the carrier' of X1 & G " is one-to-one & ( for s1 being stack of X2
for s2 being stack of X1 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 X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) ) ) )
thus
( dom (G ") = the carrier' of X2 & rng (G ") = the carrier' of X1 & G " is one-to-one )
by A2, FUNCT_1:33; for s1 being stack of X2
for s2 being stack of X1 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 X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) )
let s1 be stack of X2; for s2 being stack of X1 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 X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) )
let s2 be stack of X1; ( s2 = (G ") . s1 implies ( ( 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 X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) ) )
assume
s2 = (G ") . s1
; ( ( 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 X2
for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1)) ) )
then A4:
G . s2 = s1
by A2, FUNCT_1:35;
hence A5:
( emp s1 iff emp s2 )
by A3; ( not emp s1 iff ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) )
let e1 be Element of X2; for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1))
let e2 be Element of X1; ( e2 = (F ") . e1 implies push (e2,s2) = (G ") . (push (e1,s1)) )
assume
e2 = (F ") . e1
; push (e2,s2) = (G ") . (push (e1,s1))
then
F . e2 = e1
by A1, FUNCT_1:35;
then
G . (push (e2,s2)) = push (e1,s1)
by A3, A4;
hence
push (e2,s2) = (G ") . (push (e1,s1))
by A2, FUNCT_1:34; verum