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 A1, Th13;

A4: H is_homomorphism U1,U2 by A1, Th13;

for o being OperSymbol of S st Args (o,U2) <> {} holds

for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)

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 A1, Th13;

A4: H is_homomorphism U1,U2 by A1, Th13;

for o being OperSymbol of S st Args (o,U2) <> {} holds

for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)

proof

hence
H "" is_homomorphism U2,U1
; :: thesis: verum
let o be OperSymbol of S; :: thesis: ( Args (o,U2) <> {} implies for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) )

assume Args (o,U2) <> {} ; :: thesis: for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)

let x be Element of Args (o,U2); :: thesis: ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)

set r = the_result_sort_of o;

deffunc H_{1}( object ) -> set = ((H "") # x) . $1;

consider f being Function such that

A5: ( dom f = dom (the_arity_of o) & ( for n being object st n in dom (the_arity_of o) holds

f . n = H_{1}(n) ) )
from FUNCT_1:sch 3();

A6: dom ((H "") # x) = dom (the_arity_of o) by Th6;

then A7: f = (H "") # x by A5, FUNCT_1:2;

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 . (the_result_sort_of o) is one-to-one by A3;

( dom (H . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) & (H "") . (the_result_sort_of o) = (H . (the_result_sort_of o)) " ) by A2, A3, Def4, FUNCT_2:def 1;

then A9: ((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o)) = id ( the Sorts of U1 . (the_result_sort_of o)) by A8, FUNCT_1:39;

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 A10, A11, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

reconsider f = f as Element of Args (o,U1) by A5, A6, FUNCT_1:2;

A13: dom (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def 1;

(H . (the_result_sort_of o)) . ((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 "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) . ((Den (o,U1)) . ((H "") # x)) by A7, A13, A12, FUNCT_1:12

.= (Den (o,U1)) . ((H "") # x) by A12, A9 ;

hence ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) ; :: thesis: verum

end;assume Args (o,U2) <> {} ; :: thesis: for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)

let x be Element of Args (o,U2); :: thesis: ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)

set r = the_result_sort_of o;

deffunc H

consider f being Function such that

A5: ( dom f = dom (the_arity_of o) & ( for n being object st n in dom (the_arity_of o) holds

f . n = H

A6: dom ((H "") # x) = dom (the_arity_of o) by Th6;

then A7: f = (H "") # x by A5, FUNCT_1:2;

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 . (the_result_sort_of o) is one-to-one by A3;

( dom (H . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) & (H "") . (the_result_sort_of o) = (H . (the_result_sort_of o)) " ) by A2, A3, Def4, FUNCT_2:def 1;

then A9: ((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o)) = id ( the Sorts of U1 . (the_result_sort_of o)) by A8, FUNCT_1:39;

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 A10, A11, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def 2 ;

reconsider f = f as Element of Args (o,U1) by A5, A6, FUNCT_1:2;

A13: dom (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def 1;

(H . (the_result_sort_of o)) . ((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 "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) . ((Den (o,U1)) . ((H "") # x)) by A7, A13, A12, FUNCT_1:12

.= (Den (o,U1)) . ((H "") # x) by A12, A9 ;

hence ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) ; :: thesis: verum