let X1, X2 be StackAlgebra; :: thesis: ( 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 ; :: according to STACKS_1:def 22 :: thesis: ( not X1 is proper-for-identity or X2 is proper-for-identity )
assume A2: X1 is proper-for-identity ; :: thesis: X2 is proper-for-identity
let s1, s2 be stack of X2; :: according to STACKS_1:def 15 :: thesis: ( 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.| ; :: according to STACKS_1:def 14 :: thesis: 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; :: thesis: verum