:: deftheorem defines are_os_isomorphic OSALG_3:def 2 :
for S1 being OrderSortedSign
for U1, U2 being OSAlgebra of S1 holds
( U1,U2 are_os_isomorphic iff ex F being ManySortedFunction of U1,U2 st
( F is_isomorphism U1,U2 & F is order-sorted ) );