let S1 be OrderSortedSign; :: thesis: for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds

U1,U3 are_os_isomorphic

let U1, U2, U3 be non-empty OSAlgebra of S1; :: thesis: ( U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic implies U1,U3 are_os_isomorphic )

assume that

A1: U1,U2 are_os_isomorphic and

A2: U2,U3 are_os_isomorphic ; :: thesis: U1,U3 are_os_isomorphic

consider F being ManySortedFunction of U1,U2 such that

A3: F is_isomorphism U1,U2 and

A4: F is order-sorted by A1;

consider G being ManySortedFunction of U2,U3 such that

A5: G is_isomorphism U2,U3 and

A6: G is order-sorted by A2;

reconsider H = G ** F as ManySortedFunction of U1,U3 ;

A7: H is_isomorphism U1,U3 by A3, A5, MSUALG_3:15;

A8: the Sorts of U3 is V2() OrderSortedSet of S1 by OSALG_1:17;

( the Sorts of U1 is V2() OrderSortedSet of S1 & the Sorts of U2 is V2() OrderSortedSet of S1 ) by OSALG_1:17;

then H is order-sorted by A4, A6, A8, Th5;

hence U1,U3 are_os_isomorphic by A7; :: thesis: verum

U1,U3 are_os_isomorphic

let U1, U2, U3 be non-empty OSAlgebra of S1; :: thesis: ( U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic implies U1,U3 are_os_isomorphic )

assume that

A1: U1,U2 are_os_isomorphic and

A2: U2,U3 are_os_isomorphic ; :: thesis: U1,U3 are_os_isomorphic

consider F being ManySortedFunction of U1,U2 such that

A3: F is_isomorphism U1,U2 and

A4: F is order-sorted by A1;

consider G being ManySortedFunction of U2,U3 such that

A5: G is_isomorphism U2,U3 and

A6: G is order-sorted by A2;

reconsider H = G ** F as ManySortedFunction of U1,U3 ;

A7: H is_isomorphism U1,U3 by A3, A5, MSUALG_3:15;

A8: the Sorts of U3 is V2() OrderSortedSet of S1 by OSALG_1:17;

( the Sorts of U1 is V2() OrderSortedSet of S1 & the Sorts of U2 is V2() OrderSortedSet of S1 ) by OSALG_1:17;

then H is order-sorted by A4, A6, A8, Th5;

hence U1,U3 are_os_isomorphic by A7; :: thesis: verum