theorem Th14: :: MSUALG_3:14

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1