let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of S st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic
let U1, U2 be non-empty MSAlgebra of S; :: thesis: ( U1,U2 are_isomorphic implies U2,U1 are_isomorphic )
assume U1,U2 are_isomorphic ; :: thesis: U2,U1 are_isomorphic
then consider F being ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2 by Def13;
reconsider G = F "" as ManySortedFunction of U2,U1 ;
G is_isomorphism U2,U1 by A1, Th14;
hence U2,U1 are_isomorphic by Def13; :: thesis: verum