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 non-empty OrderSortedSet of S1 by OSALG_1:17;
( the Sorts of U1 is non-empty OrderSortedSet of S1 & the Sorts of U2 is non-empty 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