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 Def7;
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; :: 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 A3: 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 object ; :: 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 Def7;
consider s being stack of X such that
A4: |.s.| = x by Th12;
x = G . s by A1, A4;
hence x in rng G by A3, 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, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom G or not y in dom 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 ;
hence x = y by Def15; :: 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 A5: 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 Th5;
hence emp s2 by A5, Def7; :: 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 Def7;
hence emp s1 by A5, Th10; :: 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) )
hence pop s2 = Del (s2,1) by A6, Def7
.= |.(pop s1).| by A5, A7, Th7
.= G . (pop s1) by A1 ;
:: thesis: top s2 = (id the carrier of X) . (top s1)
thus top s2 = s2 . 1 by A7, A6, Def7
.= top s1 by A5, A7, Th9
.= (id the carrier of X) . (top s1) ; :: 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 Def7
.= <*e1*> ^ s2
.= |.(push (e1,s1)).| by A5, Th8
.= G . (push (e1,s1)) by A1 ;
:: thesis: verum