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