let U1, U2, U3 be Universal_Algebra; ( U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic )
assume
U1,U2 are_isomorphic
; ( not U2,U3 are_isomorphic or U1,U3 are_isomorphic )
then consider f being Function of U1,U2 such that
A1:
f is_isomorphism
;
assume
U2,U3 are_isomorphic
; U1,U3 are_isomorphic
then consider g being Function of U2,U3 such that
A2:
g is_isomorphism
;
g * f is_isomorphism
by A1, A2, Th11;
hence
U1,U3 are_isomorphic
; verum