let S be non empty non void ManySortedSign ; for U1 being strict non-empty MSAlgebra of S
for U2 being non-empty MSAlgebra of 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 be strict non-empty MSAlgebra of S; for U2 being non-empty MSAlgebra of 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 U2 be non-empty MSAlgebra of 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[ set , set ] 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 set st i in the carrier of S holds
for e being set 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 7 A is_closed_on olet y be
set ;
MSUALG_2:def 6,
TARSKI:def 3 ( not y in proj2 ((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
set 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 5;
A8:
x in ((A # ) * the Arity of S) . o
by A6, RELAT_1:86;
then
x in (A # ) . (the Arity of S . o)
by FUNCT_2:21;
then
x in (A # ) . (the_arity_of o)
by MSUALG_1:def 6;
then A9:
x in product (A * (the_arity_of o))
by PBOOLE:def 19;
reconsider x =
x as
Element of
Args o,
U1 by A6;
A10:
y = (Den o,U1) . x
by A7, A8, FUNCT_1:72;
A11:
dom (h1 # x) = dom (the_arity_of o)
by MSUALG_3:6;
A12:
for
n being
set st
n in dom (h1 # x) holds
(h1 # x) . n = (h2 # x) . n
proof
let n be
set ;
( 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 13;
dom x = dom (A * (the_arity_of o))
by A9, CARD_3:18;
then
x . n in (A * (the_arity_of o)) . n
by A9, A11, A14, A13, CARD_3:18;
then
x . n in A . ((the_arity_of o) . n)
by A11, A14, FUNCT_1:23;
then
x . n in A . ((the_arity_of o) /. n)
by A11, A14, PARTFUN1:def 8;
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 8
.=
(h2 # x) . n
by A11, A14, A13, MSUALG_3:def 8
;
verum
end;
(Den o,U1) . x is
Element of
(the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 10;
then
(Den o,U1) . x is
Element of the
Sorts of
U1 . (the ResultSort of S . o)
by FUNCT_2:21;
then A15:
(Den o,U1) . x is
Element of the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 7;
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:72
.=
(Den o,U2) . (h1 # x)
by A1, MSUALG_3:def 9
.=
(Den o,U2) . (h2 # x)
by A16, A12, FUNCT_1:9, MSUALG_3:6
.=
(h2 . (the_result_sort_of o)) . ((Den o,U1) . x)
by A2, MSUALG_3:def 9
.=
(h2 . (the_result_sort_of o)) . y
by A7, A8, FUNCT_1:72
;
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 7;
hence
y in (the ResultSort of S * A) . o
by FUNCT_2:21;
verum
end;
then A17:
U1 | A = MSAlgebra(# A,(Opers U1,A) #)
by MSUALG_2:def 16;
Gen is ManySortedSubset of the Sorts of (U1 | A)
then A21:
GenMSAlg Gen is MSSubAlgebra of U1 | A
by MSUALG_2:def 18;
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 10;
then A22:
the Sorts of U1 c= A
by PBOOLE:def 23;
hence
h1 = h2
by PBOOLE:3; verum