let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of 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 of 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 )
assume A1:
H is_isomorphism U1,U2
; :: thesis: H "" is_homomorphism U2,U1
set F = H "" ;
A2:
( H is_homomorphism U1,U2 & H is "onto" & H is "1-1" )
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;
:: 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 H1(
set )
-> set =
((H "" ) # x) . $1;
consider f being
Function such that A3:
(
dom f = dom (the_arity_of o) & ( for
n being
set st
n in dom (the_arity_of o) holds
f . n = H1(
n) ) )
from FUNCT_1:sch 3();
A4:
dom ((H "" ) # x) = dom (the_arity_of o)
by Th6;
then A5:
f = (H "" ) # x
by A3, FUNCT_1:9;
reconsider f =
f as
Element of
Args o,
U1 by A3, A4, FUNCT_1:9;
the_result_sort_of o in the
carrier of
S
;
then A6:
the_result_sort_of o in dom H
by PBOOLE:def 3;
A7:
(
dom (H . (the_result_sort_of o)) = the
Sorts of
U1 . (the_result_sort_of o) &
rng (H . (the_result_sort_of o)) c= the
Sorts of
U2 . (the_result_sort_of o) )
by FUNCT_2:def 1, RELSET_1:12;
A8:
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;
A10:
(
dom the
ResultSort of
S = the
carrier' of
S &
rng the
ResultSort of
S c= the
carrier of
S )
by FUNCT_2:def 1, RELSET_1:12;
then A11:
dom (the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by PBOOLE:def 3;
A12:
Result o,
U1 =
(the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 10
.=
the
Sorts of
U1 . (the ResultSort of S . o)
by A10, A11, FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7
;
A13:
(H "" ) . (the_result_sort_of o) = (H . (the_result_sort_of o)) "
by A2, Def5;
H . (the_result_sort_of o) is
one-to-one
by A2, A6, Def2;
then A14:
((H "" ) . (the_result_sort_of o)) * (H . (the_result_sort_of o)) = id (the Sorts of U1 . (the_result_sort_of o))
by A7, A13, FUNCT_1:61;
(H . (the_result_sort_of o)) . ((Den o,U1) . f) =
(Den o,U2) . (H # ((H "" ) # x))
by A2, A5, Def9
.=
(Den o,U2) . ((H ** (H "" )) # x)
by Th8
.=
(Den o,U2) . ((id the Sorts of U2) # x)
by A2, 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 A5, A8, A12, FUNCT_1:22
.=
(Den o,U1) . ((H "" ) # x)
by A12, A14, FUNCT_1:35
;
hence
((H "" ) . (the_result_sort_of o)) . ((Den o,U2) . x) = (Den o,U1) . ((H "" ) # x)
;
:: thesis: verum
end;
hence
H "" is_homomorphism U2,U1
by Def9; :: thesis: verum