let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1

let U1, U2 be non-empty MSAlgebra over S; :: thesis: for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1

let H be ManySortedFunction of U1,U2; :: thesis: ( H is_isomorphism U1,U2 implies H "" is_homomorphism U2,U1 )
set F = H "" ;
assume A1: H is_isomorphism U1,U2 ; :: thesis: H "" is_homomorphism U2,U1
then A2: H is "onto" by Th13;
A3: H is "1-1" by ;
A4: H is_homomorphism U1,U2 by ;
for o being OperSymbol of S st Args (o,U2) <> {} holds
for x being Element of Args (o,U2) holds ((H "") . ) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)
proof
let o be OperSymbol of S; :: thesis: ( Args (o,U2) <> {} implies for x being Element of Args (o,U2) holds ((H "") . ) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) )
assume Args (o,U2) <> {} ; :: thesis: for x being Element of Args (o,U2) holds ((H "") . ) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)
let x be Element of Args (o,U2); :: thesis: ((H "") . ) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)
set r = the_result_sort_of o;
deffunc H1( object ) -> set = ((H "") # x) . \$1;
consider f being Function such that
A5: ( dom f = dom () & ( for n being object st n in dom () holds
f . n = H1(n) ) ) from A6: dom ((H "") # x) = dom () by Th6;
then A7: f = (H "") # x by ;
the_result_sort_of o in the carrier of S ;
then the_result_sort_of o in dom H by PARTFUN1:def 2;
then A8: H . is one-to-one by A3;
( dom (H . ) = the Sorts of U1 . & (H "") . = (H . ) " ) by ;
then A9: ((H "") . ) * (H . ) = id ( the Sorts of U1 . ) by ;
A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A11: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 2;
A12: Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def 5
.= the Sorts of U1 . ( the ResultSort of S . o) by
.= the Sorts of U1 . by MSUALG_1:def 2 ;
reconsider f = f as Element of Args (o,U1) by ;
A13: dom (((H "") . ) * (H . )) = the Sorts of U1 . by FUNCT_2:def 1;
(H . ) . ((Den (o,U1)) . f) = (Den (o,U2)) . (H # ((H "") # x)) by A4, A7
.= (Den (o,U2)) . ((H ** (H "")) # x) by Th8
.= (Den (o,U2)) . ((id the Sorts of U2) # x) by A2, A3, Th5
.= (Den (o,U2)) . x by Th7 ;
then ((H "") . ) . ((Den (o,U2)) . x) = (((H "") . ) * (H . )) . ((Den (o,U1)) . ((H "") # x)) by
.= (Den (o,U1)) . ((H "") # x) by ;
hence ((H "") . ) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) ; :: thesis: verum
end;
hence H "" is_homomorphism U2,U1 ; :: thesis: verum