let S be non empty non void ManySortedSign ; 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; 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; ( H is_isomorphism U1,U2 implies H "" is_homomorphism U2,U1 )
set F = H "" ;
assume A1:
H is_isomorphism U1,U2
; 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
let o be
OperSymbol of
S;
( 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)
<> {}
;
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);
((H "") . (the_result_sort_of o)) . ((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 (the_arity_of o) & ( for
n being
object st
n in dom (the_arity_of o) holds
f . n = H1(
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)
;
verum
end;
hence
H "" is_homomorphism U2,U1
; verum