let X1, X2 be StackAlgebra; :: thesis: 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; :: thesis: ( 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)) ) ) ; :: according to STACKS_1:def 21 :: thesis: 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; :: according to STACKS_1:def 21 :: thesis: ( 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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; :: thesis: ( not emp s1 iff ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) )

hereby :: thesis: 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 not emp s1 ; :: thesis: ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) )
then ( pop s1 = G . (pop s2) & top s1 = F . (top s2) ) by A3, A5, A4;
hence ( pop s2 = (G ") . (pop s1) & top s2 = (F ") . (top s1) ) by A1, A2, FUNCT_1:34; :: thesis: verum

end;

let e1 be Element of X2; :: thesis: for e2 being Element of X1 st e2 = (F ") . e1 holds
push (e2,s2) = (G ") . (push (e1,s1))
let e2 be Element of X1; :: thesis: ( e2 = (F ") . e1 implies push (e2,s2) = (G ") . (push (e1,s1)) )
assume e2 = (F ") . e1 ; :: thesis: 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; :: thesis: verum