let X be proper-for-identity StackAlgebra; :: thesis: ex G being Function st
( ( for s being stack of X holds G . s = |.s.| ) & id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )
deffunc H₁( stack of X) -> Element of the carrier of X * = |.$1.|;
consider G being Function of the carrier' of X,( the carrier of X *) such that
A1: for s being stack of X holds G . s = H₁(s) from FUNCT_2:sch 4();
take G ; :: thesis: ( ( for s being stack of X holds G . s = |.s.| ) & id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X )
thus for s being stack of X holds G . s = |.s.| by A1; :: thesis: id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X
set F = id the carrier of X;
set X2 = StandardStackSystem the carrier of X;
set A = the carrier of X;
A2: ( the carrier of (StandardStackSystem the carrier of X) = the carrier of X & the carrier' of (StandardStackSystem the carrier of X) = the carrier of X * & ( for s being stack of (StandardStackSystem the carrier of X) holds
( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( for g being FinSequence st g = s holds
( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of (StandardStackSystem the carrier of X) & pop s = {} ) ) & ( for e being Element of (StandardStackSystem the carrier of X) holds push (e,s) = <*e*> ^ g ) ) ) ) ) ) by EXAM;
thus ( dom (id the carrier of X) = the carrier of X & rng (id the carrier of X) = the carrier of (StandardStackSystem the carrier of X) & id the carrier of X is one-to-one ) by A2, RELAT_1:45; :: according to STACKS_1:def 21 :: thesis: ( dom G = the carrier' of X & rng G = the carrier' of (StandardStackSystem the carrier of X) & G is one-to-one & ( for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) )
thus A4: dom G = the carrier' of X by FUNCT_2:def 1; :: thesis: ( rng G = the carrier' of (StandardStackSystem the carrier of X) & G is one-to-one & ( for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) )
thus rng G = the carrier' of (StandardStackSystem the carrier of X) :: thesis: ( G is one-to-one & ( for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) ) ) )

proof

thus rng G c= the carrier' of (StandardStackSystem the carrier of X) by A2; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of (StandardStackSystem the carrier of X) c= rng G
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of (StandardStackSystem the carrier of X) or x in rng G )
assume x in the carrier' of (StandardStackSystem the carrier of X) ; :: thesis: x in rng G
then reconsider x = x as Element of the carrier of X * by EXAM;
consider s being stack of X such that
A3: |.s.| = x by Th36;
x = G . s by A1, A3;
hence x in rng G by A4, FUNCT_1:def 3; :: thesis: verum

end;

thus G is one-to-one :: thesis: for s1 being stack of X
for s2 being stack of (StandardStackSystem the carrier of X) 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 G or not b₁ in proj1 G or not G . x = G . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 G or not y in proj1 G or not G . x = G . y or x = y )
assume ( x in dom G & y in dom G ) ; :: thesis: ( not G . x = G . y or x = y )
then reconsider s1 = x, s2 = y as stack of X ;
assume G . x = G . y ; :: thesis: x = y
then |.s1.| = G . y by A1
.= |.s2.| by A1 ;
then s1 == s2 by CONG;
hence x = y by PROP; :: thesis: verum

end;

let s1 be stack of X; :: thesis: for s2 being stack of (StandardStackSystem the carrier of X) 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
let s2 be stack of (StandardStackSystem the carrier of X); :: 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . 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 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )
then A6: s2 = |.s1.| by A1;

hereby :: thesis: ( ( emp s2 implies emp s1 ) & ( not emp s1 implies ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) ) & ( for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1)) ) )

assume emp s1 ; :: thesis: emp s2
then |.s1.| = {} by Th31;
hence emp s2 by A6, EXAM; :: thesis: verum

end;

hereby :: thesis: ( not emp s1 iff ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) ) )

assume emp s2 ; :: thesis: emp s1
then s2 = {} by EXAM;
hence emp s1 by A6, Th351; :: thesis: verum

end;

hereby :: thesis: for e1 being Element of X
for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1))

assume A7: not emp s1 ; :: thesis: ( pop s2 = G . (pop s1) & top s2 = (id the carrier of X) . (top s1) )
thus pop s2 = Del (s2,1) by A7, A8, EXAM
.= |.(pop s1).| by A6, A7, Th33
.= G . (pop s1) by A1 ; :: thesis: top s2 = (id the carrier of X) . (top s1)
thus top s2 = s2 . 1 by A7, A8, EXAM
.= top s1 by A6, A7, Th35
.= (id the carrier of X) . (top s1) by FUNCT_1:18 ; :: thesis: verum

end;

let e1 be Element of X; :: thesis: for e2 being Element of (StandardStackSystem the carrier of X) st e2 = (id the carrier of X) . e1 holds
push (e2,s2) = G . (push (e1,s1))
let e2 be Element of (StandardStackSystem the carrier of X); :: thesis: ( e2 = (id the carrier of X) . e1 implies push (e2,s2) = G . (push (e1,s1)) )
assume e2 = (id the carrier of X) . e1 ; :: thesis: push (e2,s2) = G . (push (e1,s1))
hence push (e2,s2) = <*((id the carrier of X) . e1)*> ^ s2 by EXAM
.= <*e1*> ^ s2 by FUNCT_1:18
.= |.(push (e1,s1)).| by A6, Th34
.= G . (push (e1,s1)) by A1 ;
:: thesis: verum