let X1, X2, X3 be StackAlgebra; :: thesis: ( X1,X2 are_isomorphic & X2,X3 are_isomorphic implies X1,X3 are_isomorphic )
given F1, G1 being Function such that A1: F1,G1 form_isomorphism_between X1,X2 ; :: according to STACKS_1:def 22 :: thesis: ( not X2,X3 are_isomorphic or X1,X3 are_isomorphic )
given F2, G2 being Function such that A2: F2,G2 form_isomorphism_between X2,X3 ; :: according to STACKS_1:def 22 :: thesis: X1,X3 are_isomorphic
take F2 * F1 ; :: according to STACKS_1:def 22 :: thesis: ex G being Function st F2 * F1,G form_isomorphism_between X1,X3
take G2 * G1 ; :: thesis: F2 * F1,G2 * G1 form_isomorphism_between X1,X3
thus F2 * F1,G2 * G1 form_isomorphism_between X1,X3 by A1, A2, Th44; :: thesis: verum