let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over S
for Gen being GeneratorSet of U1
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds
h1 = h2
let U1, U2 be non-empty MSAlgebra over S; for Gen being GeneratorSet of U1
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds
h1 = h2
let Gen be GeneratorSet of U1; for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds
h1 = h2
let h1, h2 be ManySortedFunction of U1,U2; ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen implies h1 = h2 )
assume that
A1:
h1 is_homomorphism U1,U2
and
A2:
h2 is_homomorphism U1,U2
and
A3:
h1 || Gen = h2 || Gen
; h1 = h2
defpred S1[ object , object ] means ex s being SortSymbol of S st
( $1 = s & (h1 . s) . $2 = (h2 . s) . $2 );
set I = the carrier of S;
consider A being ManySortedSet of the carrier of S such that
A4:
for i being object st i in the carrier of S holds
for e being object holds
( e in A . i iff ( e in the Sorts of U1 . i & S1[i,e] ) )
from PBOOLE:sch 2();
A is ManySortedSubset of the Sorts of U1
then reconsider A = A as MSSubset of U1 ;
A is opers_closed
proof
let o be
OperSymbol of
S;
MSUALG_2:def 6 A is_closed_on olet y be
object ;
MSUALG_2:def 5,
TARSKI:def 3 ( not y in rng ((Den (o,U1)) | (( the Arity of S * (A #)) . o)) or y in ( the ResultSort of S * A) . o )
set r =
the_result_sort_of o;
set ar =
the_arity_of o;
assume
y in rng ((Den (o,U1)) | (((A #) * the Arity of S) . o))
;
y in ( the ResultSort of S * A) . o
then consider x being
object such that A6:
x in dom ((Den (o,U1)) | (((A #) * the Arity of S) . o))
and A7:
((Den (o,U1)) | (((A #) * the Arity of S) . o)) . x = y
by FUNCT_1:def 3;
A8:
x in ((A #) * the Arity of S) . o
by A6, RELAT_1:57;
then
x in (A #) . ( the Arity of S . o)
by FUNCT_2:15;
then
x in (A #) . (the_arity_of o)
by MSUALG_1:def 1;
then A9:
x in product (A * (the_arity_of o))
by FINSEQ_2:def 5;
reconsider x =
x as
Element of
Args (
o,
U1)
by A6;
A10:
y = (Den (o,U1)) . x
by A7, A8, FUNCT_1:49;
A11:
dom (h1 # x) = dom (the_arity_of o)
by MSUALG_3:6;
A12:
for
n being
object st
n in dom (h1 # x) holds
(h1 # x) . n = (h2 # x) . n
proof
let n be
object ;
( n in dom (h1 # x) implies (h1 # x) . n = (h2 # x) . n )
A13:
dom x = dom (the_arity_of o)
by MSUALG_3:6;
assume A14:
n in dom (h1 # x)
;
(h1 # x) . n = (h2 # x) . n
then reconsider n9 =
n as
Nat by A11, ORDINAL1:def 12;
dom x = dom (A * (the_arity_of o))
by A9, CARD_3:9;
then
x . n in (A * (the_arity_of o)) . n
by A9, A11, A14, A13, CARD_3:9;
then
x . n in A . ((the_arity_of o) . n)
by A11, A14, FUNCT_1:13;
then
x . n in A . ((the_arity_of o) /. n)
by A11, A14, PARTFUN1:def 6;
then
ex
s being
SortSymbol of
S st
(
s = (the_arity_of o) /. n &
(h1 . s) . (x . n) = (h2 . s) . (x . n) )
by A4;
hence (h1 # x) . n =
(h2 . ((the_arity_of o) /. n)) . (x . n9)
by A11, A14, A13, MSUALG_3:def 6
.=
(h2 # x) . n
by A11, A14, A13, MSUALG_3:def 6
;
verum
end;
(Den (o,U1)) . x is
Element of
( the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 5;
then
(Den (o,U1)) . x is
Element of the
Sorts of
U1 . ( the ResultSort of S . o)
by FUNCT_2:15;
then A15:
(Den (o,U1)) . x is
Element of the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 2;
A16:
dom (h2 # x) = dom (the_arity_of o)
by MSUALG_3:6;
(h1 . (the_result_sort_of o)) . y =
(h1 . (the_result_sort_of o)) . ((Den (o,U1)) . x)
by A7, A8, FUNCT_1:49
.=
(Den (o,U2)) . (h1 # x)
by A1
.=
(Den (o,U2)) . (h2 # x)
by A16, A12, FUNCT_1:2, MSUALG_3:6
.=
(h2 . (the_result_sort_of o)) . ((Den (o,U1)) . x)
by A2
.=
(h2 . (the_result_sort_of o)) . y
by A7, A8, FUNCT_1:49
;
then
y in A . (the_result_sort_of o)
by A4, A10, A15;
then
y in A . ( the ResultSort of S . o)
by MSUALG_1:def 2;
hence
y in ( the ResultSort of S * A) . o
by FUNCT_2:15;
verum
end;
then A17:
U1 | A = MSAlgebra(# A,(Opers (U1,A)) #)
by MSUALG_2:def 15;
Gen is ManySortedSubset of the Sorts of (U1 | A)
then A21:
GenMSAlg Gen is MSSubAlgebra of U1 | A
by MSUALG_2:def 17;
the Sorts of (GenMSAlg Gen) = the Sorts of U1
by MSAFREE:def 4;
then
the Sorts of U1 is ManySortedSubset of A
by A17, A21, MSUALG_2:def 9;
then A22:
the Sorts of U1 c= A
by PBOOLE:def 18;
hence
h1 = h2
; verum