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

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