let X be proper-for-identity StackAlgebra; :: thesis: X, StandardStackSystem the carrier of X are_isomorphic
consider G being Function such that
for s being stack of X holds G . s = |.s.| and
A1: id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X by Th48;
take id the carrier of X ; :: according to STACKS_1:def 22 :: thesis: ex G being Function st id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X
take G ; :: thesis: id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X
thus id the carrier of X,G form_isomorphism_between X, StandardStackSystem the carrier of X by A1; :: thesis: verum