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

U2,U1 are_os_isomorphic

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

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

assume U1,U2 are_os_isomorphic ; :: thesis: U2,U1 are_os_isomorphic

then consider F being ManySortedFunction of U1,U2 such that

A2: F is_isomorphism U1,U2 and

A3: F is order-sorted ;

reconsider G = F "" as ManySortedFunction of U2,U1 ;

A4: G is_isomorphism U2,U1 by A2, MSUALG_3:14;

( F is "onto" & F is "1-1" ) by A2, MSUALG_3:13;

then F "" is order-sorted by A3, A1, Th6;

hence U2,U1 are_os_isomorphic by A4; :: thesis: verum

U2,U1 are_os_isomorphic

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

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

assume U1,U2 are_os_isomorphic ; :: thesis: U2,U1 are_os_isomorphic

then consider F being ManySortedFunction of U1,U2 such that

A2: F is_isomorphism U1,U2 and

A3: F is order-sorted ;

reconsider G = F "" as ManySortedFunction of U2,U1 ;

A4: G is_isomorphism U2,U1 by A2, MSUALG_3:14;

( F is "onto" & F is "1-1" ) by A2, MSUALG_3:13;

then F "" is order-sorted by A3, A1, Th6;

hence U2,U1 are_os_isomorphic by A4; :: thesis: verum