let S be non empty non void ManySortedSign ; for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic
let U1, U2, U3 be non-empty MSAlgebra over S; ( U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic )
assume that
A1:
U1,U2 are_isomorphic
and
A2:
U2,U3 are_isomorphic
; U1,U3 are_isomorphic
consider F being ManySortedFunction of U1,U2 such that
A3:
F is_isomorphism U1,U2
by A1;
consider G being ManySortedFunction of U2,U3 such that
A4:
G is_isomorphism U2,U3
by A2;
reconsider H = G ** F as ManySortedFunction of U1,U3 ;
H is_isomorphism U1,U3
by A3, A4, Th15;
hence
U1,U3 are_isomorphic
; verum