let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum