let X1, X2 be StackAlgebra; ( X1,X2 are_isomorphic & X1 is proper-for-identity implies X2 is proper-for-identity )
given F, G being Function such that A1:
F,G form_isomorphism_between X1,X2
; STACKS_1:def 22 ( not X1 is proper-for-identity or X2 is proper-for-identity )
assume A2:
X1 is proper-for-identity
; X2 is proper-for-identity
let s1, s2 be stack of X2; STACKS_1:def 15 ( s1 == s2 implies s1 = s2 )
A3:
( dom G = the carrier' of X1 & rng G = the carrier' of X2 )
by A1;
then consider q1 being object such that
A4:
( q1 in dom G & s1 = G . q1 )
by FUNCT_1:def 3;
consider q2 being object such that
A5:
( q2 in dom G & s2 = G . q2 )
by A3, FUNCT_1:def 3;
reconsider q1 = q1, q2 = q2 as stack of X1 by A1, A4, A5;
A6:
( dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one )
by A1;
A7:
( rng |.q1.| c= the carrier of X1 & rng |.q2.| c= the carrier of X1 )
;
assume
|.s1.| = |.s2.|
; STACKS_1:def 14 s1 = s2
then A8: F * |.q1.| =
|.s2.|
by A1, A4, Th45
.=
F * |.q2.|
by A1, A5, Th45
;
( dom (F * |.q1.|) = dom |.q1.| & dom (F * |.q2.|) = dom |.q2.| )
by A6, A7, RELAT_1:27;
then
|.q1.| = |.q2.|
by A6, A7, A8, FUNCT_1:27;
then
q1 == q2
;
hence
s1 = s2
by A2, A4, A5; verum