let I be non empty set ; for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let A be MSAlgebra-Family of I,S; for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let U1 be non-empty MSAlgebra over S; for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
let F be ManySortedFunction of I; ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) )
assume A1:
for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i )
; ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
set SU = the Sorts of U1;
set CA = the carrier of S;
set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ;
deffunc H1( Element of S) -> set = commute ((commute F) . $1);
consider H being ManySortedSet of the carrier of S such that
A2:
for s9 being Element of the carrier of S holds H . s9 = H1(s9)
from PBOOLE:sch 5();
now for s9 being object st s9 in the carrier of S holds
H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9)let s9 be
object ;
( s9 in the carrier of S implies H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) )assume A3:
s9 in the
carrier of
S
;
H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9)then reconsider s99 =
s9 as
SortSymbol of
S ;
(commute F) . s9 in Funcs (
I,
(Funcs (( the Sorts of U1 . s9),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
by A1, A3, Th26;
then
commute ((commute F) . s9) in Funcs (
( the Sorts of U1 . s9),
(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
by A3, FUNCT_6:55;
then
H . s9 in Funcs (
( the Sorts of U1 . s9),
(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
by A2, A3;
then consider Hs being
Function such that A4:
Hs = H . s9
and A5:
dom Hs = the
Sorts of
U1 . s9
and A6:
rng Hs c= Funcs (
I,
(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))
by FUNCT_2:def 2;
rng Hs c= the
Sorts of
(product A) . s9
proof
let x be
object ;
TARSKI:def 3 ( not x in rng Hs or x in the Sorts of (product A) . s9 )
assume A7:
x in rng Hs
;
x in the Sorts of (product A) . s9
then consider f being
Function such that A8:
f = x
and A9:
dom f = I
and
rng f c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum }
by A6, FUNCT_2:def 2;
consider x1 being
object such that A10:
x1 in dom Hs
and A11:
Hs . x1 = f
by A7, A8, FUNCT_1:def 3;
A12:
now for i9 being object st i9 in dom (Carrier (A,s99)) holds
f . i9 in (Carrier (A,s99)) . i9let i9 be
object ;
( i9 in dom (Carrier (A,s99)) implies f . i9 in (Carrier (A,s99)) . i9 )assume
i9 in dom (Carrier (A,s99))
;
f . i9 in (Carrier (A,s99)) . i9then reconsider i99 =
i9 as
Element of
I ;
consider F9 being
ManySortedFunction of
U1,
(A . i99) such that A13:
F9 = F . i99
and
F9 is_homomorphism U1,
A . i99
by A1;
H . s99 = commute ((commute F) . s99)
by A2;
then A14:
f . i99 = (F9 . s99) . x1
by A1, A4, A5, A10, A11, A13, Th27;
dom (F9 . s99) = dom Hs
by A5, FUNCT_2:def 1;
then A15:
(F9 . s9) . x1 in rng (F9 . s9)
by A10, FUNCT_1:def 3;
( ex
U0 being
MSAlgebra over
S st
(
U0 = A . i99 &
(Carrier (A,s99)) . i99 = the
Sorts of
U0 . s99 ) &
rng (F9 . s99) c= the
Sorts of
(A . i99) . s99 )
by PRALG_2:def 9;
hence
f . i9 in (Carrier (A,s99)) . i9
by A14, A15;
verum end;
dom (Carrier (A,s99)) = dom f
by A9, PARTFUN1:def 2;
then
f in product (Carrier (A,s99))
by A12, CARD_3:9;
hence
x in the
Sorts of
(product A) . s9
by A8, PRALG_2:def 10;
verum
end; hence
H . s9 is
Function of
( the Sorts of U1 . s9),
( the Sorts of (product A) . s9)
by A3, A4, A5, FUNCT_2:def 1, RELSET_1:4;
verum end;
then reconsider H = H as ManySortedFunction of U1,(product A) by PBOOLE:def 15;
A16:
H is_homomorphism U1, product A
proof
let o be
OperSymbol of
S;
MSUALG_3:def 7 ( Args (o,U1) = {} or for b1 being Element of Args (o,U1) holds (H . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,(product A))) . (H # b1) )
assume
Args (
o,
U1)
<> {}
;
for b1 being Element of Args (o,U1) holds (H . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,(product A))) . (H # b1)
let x be
Element of
Args (
o,
U1);
(H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
set s9 =
the_result_sort_of o;
A17:
Result (
o,
U1)
= the
Sorts of
U1 . (the_result_sort_of o)
by PRALG_2:3;
then A18:
(Den (o,U1)) . x in the
Sorts of
U1 . (the_result_sort_of o)
;
thus
(H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
verumproof
per cases
( the_arity_of o = {} or the_arity_of o <> {} )
;
suppose A19:
the_arity_of o = {}
;
(H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)set f =
(commute ((commute F) . (the_result_sort_of o))) . (const (o,U1));
Args (
o,
U1)
= {{}}
by A19, PRALG_2:4;
then A20:
x = {}
by TARSKI:def 1;
A21:
now for i9 being object st i9 in I holds
((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9let i9 be
object ;
( i9 in I implies ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9 )assume
i9 in I
;
((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9then reconsider ii =
i9 as
Element of
I ;
consider F1 being
ManySortedFunction of
U1,
(A . ii) such that A22:
F1 = F . ii
and A23:
F1 is_homomorphism U1,
A . ii
by A1;
A24:
F1 # x = {}
by A19, A20, Th11;
thus ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 =
(F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x)
by A1, A17, A20, A22, Th27
.=
const (
o,
(A . ii))
by A23, A24
.=
(const (o,(product A))) . i9
by A19, Th9
;
verum end;
const (
o,
(product A))
in Funcs (
I,
(union { (Result (o,(A . i1))) where i1 is Element of I : verum } ))
by A19, Th8;
then A25:
ex
Co being
Function st
(
Co = const (
o,
(product A)) &
dom Co = I &
rng Co c= union { (Result (o,(A . i1))) where i1 is Element of I : verum } )
by FUNCT_2:def 2;
(commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) in product (Carrier (A,(the_result_sort_of o)))
by A1, A18, A20, Th28;
then
dom ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) = I
by PARTFUN1:def 2;
then A26:
(commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) = const (
o,
(product A))
by A25, A21;
H # x = {}
by A19, A20, Th11;
hence
(H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
by A2, A20, A26;
verum end; suppose A27:
the_arity_of o <> {}
;
(H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)A28:
Den (
o,
(product A)) =
(OPS A) . o
by MSUALG_1:def 6
.=
IFEQ (
(the_arity_of o),
{},
(commute (A ?. o)),
(Commute (Frege (A ?. o))))
by PRALG_2:def 13
.=
Commute (Frege (A ?. o))
by A27, FUNCOP_1:def 8
;
then reconsider f1 =
(Den (o,(product A))) . (H # x) as
Function by PRALG_2:8;
f1 in rng (Frege (A ?. o))
by A29;
then A31:
dom f1 = I
by PRALG_2:9;
set D =
union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ;
set f =
(commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x);
A32:
H # x in Funcs (
(dom (the_arity_of o)),
(Funcs (I,(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ))))
by Th14;
A33:
now for i9 being object st i9 in I holds
((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9let i9 be
object ;
( i9 in I implies ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 )assume
i9 in I
;
((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9then reconsider ii =
i9 as
Element of
I ;
consider F1 being
ManySortedFunction of
U1,
(A . ii) such that A34:
F1 = F . ii
and A35:
F1 is_homomorphism U1,
A . ii
by A1;
A36:
(F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(A . ii))) . (F1 # x)
by A35;
x in Args (
o,
U1)
;
then A40:
x in product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:3;
then A41:
dom x = dom ( the Sorts of U1 * (the_arity_of o))
by CARD_3:9;
A42:
dom x = dom (the_arity_of o)
by MSUALG_6:2;
A37:
now for n being object st n in dom (the_arity_of o) holds
((commute (H # x)) . ii) . n = (F1 # x) . nlet n be
object ;
( n in dom (the_arity_of o) implies ((commute (H # x)) . ii) . n = (F1 # x) . n )assume A38:
n in dom (the_arity_of o)
;
((commute (H # x)) . ii) . n = (F1 # x) . nthen
(the_arity_of o) . n in rng (the_arity_of o)
by FUNCT_1:def 3;
then reconsider s1 =
(the_arity_of o) . n as
Element of the
carrier of
S ;
A39:
(F1 # x) . n =
(F1 . ((the_arity_of o) /. n)) . (x . n)
by A38, Th13
.=
(F1 . s1) . (x . n)
by A38, PARTFUN1:def 6
;
x . n in ( the Sorts of U1 * (the_arity_of o)) . n
by A38, A40, A41, A42, CARD_3:9;
then A43:
x . n in the
Sorts of
U1 . s1
by A38, A42, A41, FUNCT_1:12;
A44:
(H # x) . n =
(H . ((the_arity_of o) /. n)) . (x . n)
by A38, Th13
.=
(H . s1) . (x . n)
by A38, PARTFUN1:def 6
.=
(commute ((commute F) . s1)) . (x . n)
by A2
;
then reconsider g =
(H # x) . n as
Function ;
thus ((commute (H # x)) . ii) . n =
g . ii
by A32, A38, FUNCT_6:56
.=
(F1 # x) . n
by A1, A34, A43, A39, A44, Th27
;
verum end;
dom F1 = the
carrier of
S
by PARTFUN1:def 2;
then A45:
rng (the_arity_of o) c= dom F1
;
commute (H # x) in Funcs (
I,
(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ))))
by A27, A32, FUNCT_6:55;
then consider ff being
Function such that A46:
ff = commute (H # x)
and A47:
dom ff = I
and A48:
rng ff c= Funcs (
(dom (the_arity_of o)),
(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ))
by FUNCT_2:def 2;
ff . ii in rng ff
by A47, FUNCT_1:def 3;
then A49:
ex
gg being
Function st
(
gg = (commute (H # x)) . ii &
dom gg = dom (the_arity_of o) &
rng gg c= union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )
by A46, A48, FUNCT_2:def 2;
A50:
x in product (doms (F1 * (the_arity_of o)))
by Th12;
dom (F1 # x) =
dom ((Frege (F1 * (the_arity_of o))) . x)
by MSUALG_3:def 5
.=
dom ((F1 * (the_arity_of o)) .. x)
by A50, PRALG_2:def 2
.=
(dom (F1 * (the_arity_of o))) /\ (dom x)
by PRALG_1:def 19
.=
(dom (the_arity_of o)) /\ (dom x)
by A45, RELAT_1:27
.=
dom (the_arity_of o)
by A42
;
then
F1 # x = (commute (H # x)) . ii
by A49, A37;
then ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 =
(Den (o,(A . ii))) . ((commute (H # x)) . ii)
by A1, A17, A34, A36, Th27
.=
f1 . i9
by A27, Th22
;
hence
((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9
;
verum end;
(commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) in product (Carrier (A,(the_result_sort_of o)))
by A1, A17, Th28;
then
dom ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) = I
by PARTFUN1:def 2;
then
(commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) = f1
by A31, A33;
hence
(H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x)
by A2;
verum end; end;
end;
end;
take
H
; ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
for i being Element of I holds (proj (A,i)) ** H = F . i
proof
let i be
Element of
I;
(proj (A,i)) ** H = F . i
consider F1 being
ManySortedFunction of
U1,
(A . i) such that A51:
F1 = F . i
and
F1 is_homomorphism U1,
A . i
by A1;
A52:
dom ((proj (A,i)) ** H) =
(dom (proj (A,i))) /\ (dom H)
by PBOOLE:def 19
.=
the
carrier of
S /\ (dom H)
by PARTFUN1:def 2
.=
the
carrier of
S /\ the
carrier of
S
by PARTFUN1:def 2
.=
the
carrier of
S
;
A53:
now for s9 being object st s9 in the carrier of S holds
((proj (A,i)) ** H) . s9 = F1 . s9let s9 be
object ;
( s9 in the carrier of S implies ((proj (A,i)) ** H) . s9 = F1 . s9 )assume
s9 in the
carrier of
S
;
((proj (A,i)) ** H) . s9 = F1 . s9then reconsider s1 =
s9 as
SortSymbol of
S ;
A54:
((proj (A,i)) ** H) . s9 =
((proj (A,i)) . s1) * (H . s1)
by A52, PBOOLE:def 19
.=
(proj ((Carrier (A,s1)),i)) * (H . s1)
by Def2
.=
(proj ((Carrier (A,s1)),i)) * (commute ((commute F) . s1))
by A2
;
(commute F) . s1 in Funcs (
I,
(Funcs (( the Sorts of U1 . s1),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
by A1, Th26;
then
commute ((commute F) . s1) in Funcs (
( the Sorts of U1 . s1),
(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
by FUNCT_6:55;
then consider f9 being
Function such that A55:
f9 = commute ((commute F) . s1)
and A56:
dom f9 = the
Sorts of
U1 . s1
and
rng f9 c= Funcs (
I,
(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))
by FUNCT_2:def 2;
rng f9 c= dom (proj ((Carrier (A,s1)),i))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng f9 or y in dom (proj ((Carrier (A,s1)),i)) )
assume
y in rng f9
;
y in dom (proj ((Carrier (A,s1)),i))
then consider x9 being
object such that A57:
x9 in dom f9
and A58:
f9 . x9 = y
by FUNCT_1:def 3;
(commute ((commute F) . s1)) . x9 in product (Carrier (A,s1))
by A1, A56, A57, Th28;
hence
y in dom (proj ((Carrier (A,s1)),i))
by A55, A58, CARD_3:def 16;
verum
end; then A59:
dom (((proj (A,i)) ** H) . s9) = the
Sorts of
U1 . s9
by A55, A56, A54, RELAT_1:27;
A60:
now for x being object st x in the Sorts of U1 . s9 holds
(((proj (A,i)) ** H) . s9) . x = (F1 . s9) . xlet x be
object ;
( x in the Sorts of U1 . s9 implies (((proj (A,i)) ** H) . s9) . x = (F1 . s9) . x )assume A61:
x in the
Sorts of
U1 . s9
;
(((proj (A,i)) ** H) . s9) . x = (F1 . s9) . xthen
(commute ((commute F) . s1)) . x in product (Carrier (A,s1))
by A1, Th28;
then A62:
(commute ((commute F) . s1)) . x in dom (proj ((Carrier (A,s1)),i))
by CARD_3:def 16;
thus (((proj (A,i)) ** H) . s9) . x =
(proj ((Carrier (A,s1)),i)) . ((commute ((commute F) . s1)) . x)
by A54, A59, A61, FUNCT_1:12
.=
((commute ((commute F) . s1)) . x) . i
by A62, CARD_3:def 16
.=
(F1 . s9) . x
by A1, A51, A61, Th27
;
verum end; dom (F1 . s9) =
dom (F1 . s1)
.=
the
Sorts of
U1 . s9
by FUNCT_2:def 1
;
hence
((proj (A,i)) ** H) . s9 = F1 . s9
by A59, A60;
verum end;
dom F1 = the
carrier of
S
by PARTFUN1:def 2;
hence
(proj (A,i)) ** H = F . i
by A51, A52, A53;
verum
end;
hence
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
by A16; verum