let X be StackAlgebra; :: thesis: id the carrier of X, id the carrier' of X form_isomorphism_between X,X
set F = id the carrier of X;
set G = id the carrier' of X;
thus ( dom (id the carrier of X) = the carrier of X & rng (id the carrier of X) = the carrier of X & id the carrier of X is one-to-one ) by RELAT_1:45; :: according to STACKS_1:def 21 :: thesis: ( dom (id the carrier' of X) = the carrier' of X & rng (id the carrier' of X) = the carrier' of X & id the carrier' of X is one-to-one & ( for s1, s2 being stack of X st s2 = (id the carrier' of X) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) ) ) )
thus ( dom (id the carrier' of X) = the carrier' of X & rng (id the carrier' of X) = the carrier' of X & id the carrier' of X is one-to-one ) by RELAT_1:45; :: thesis: for s1, s2 being stack of X st s2 = (id the carrier' of X) . s1 holds
( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) )
let s1, s2 be stack of X; :: thesis: ( s2 = (id the carrier' of X) . s1 implies ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) ) )
assume A0: s2 = (id the carrier' of X) . s1 ; :: thesis: ( ( emp s1 implies emp s2 ) & ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) ) )
then A1: s2 = s1 by FUNCT_1:17;
thus ( emp s1 iff emp s2 ) by A0, FUNCT_1:17; :: thesis: ( not emp s1 iff ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) )
thus ( not emp s1 implies ( pop s2 = (id the carrier' of X) . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) by A1, FUNCT_1:17; :: thesis: for e1, e2 being Element of X st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = (id the carrier' of X) . (push (e1,s1))
let e1, e2 be Element of X; :: thesis: ( e2 = (id the carrier of X) . e1 implies push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) )
assume e2 = (id the carrier of X) . e1 ; :: thesis: push (e2,s2) = (id the carrier' of X) . (push (e1,s1))
then e2 = e1 by FUNCT_1:17;
hence push (e2,s2) = (id the carrier' of X) . (push (e1,s1)) by A1, FUNCT_1:17; :: thesis: verum