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 of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of ,U1 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 of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of ,U1 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 of S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of ,U1 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 of S; for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of ,U1 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of ,U1 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 st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ex H being ManySortedFunction of ,U1 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 st
( F1 = F . i & F1 is_homomorphism U1,A . i )
; ex H being ManySortedFunction of ,U1 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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ;
deffunc H1( Element of ) -> set = commute ((commute F) . $1);
consider H being ManySortedSet of the carrier of S such that
A2:
for s' being Element of the carrier of S holds H . s' = H1(s')
from PBOOLE:sch 5();
now let s' be
set ;
( s' in the carrier of S implies H . s' is Function of the Sorts of U1 . s',the Sorts of (product A) . s' )assume A3:
s' in the
carrier of
S
;
H . s' is Function of the Sorts of U1 . s',the Sorts of (product A) . s'then reconsider s'' =
s' as
SortSymbol of ;
(commute F) . s' in Funcs I,
(Funcs (the Sorts of U1 . s'),(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
by A1, A3, Th27;
then
commute ((commute F) . s') in Funcs (the Sorts of U1 . s'),
(Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
by A3, FUNCT_6:85;
then
H . s' in Funcs (the Sorts of U1 . s'),
(Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
by A2, A3;
then consider Hs being
Function such that A4:
Hs = H . s'
and A5:
dom Hs = the
Sorts of
U1 . s'
and A6:
rng Hs c= Funcs I,
(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } )
by FUNCT_2:def 2;
rng Hs c= the
Sorts of
(product A) . s'
proof
let x be
set ;
TARSKI:def 3 ( not x in rng Hs or x in the Sorts of (product A) . s' )
assume A7:
x in rng Hs
;
x in the Sorts of (product A) . s'
then consider f being
Function such that A8:
f = x
and A9:
dom f = I
and
rng f c= union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum }
by A6, FUNCT_2:def 2;
consider x1 being
set such that A10:
x1 in dom Hs
and A11:
Hs . x1 = f
by A7, A8, FUNCT_1:def 5;
A12:
now let i' be
set ;
( i' in dom (Carrier A,s'') implies f . i' in (Carrier A,s'') . i' )assume
i' in dom (Carrier A,s'')
;
f . i' in (Carrier A,s'') . i'then reconsider i'' =
i' as
Element of
I by PARTFUN1:def 4;
consider F' being
ManySortedFunction of ,
U1 such that A13:
F' = F . i''
and
F' is_homomorphism U1,
A . i''
by A1;
H . s'' = commute ((commute F) . s'')
by A2;
then A14:
f . i'' = (F' . s'') . x1
by A1, A4, A5, A10, A11, A13, Th28;
dom (F' . s'') = dom Hs
by A5, FUNCT_2:def 1;
then A15:
(F' . s') . x1 in rng (F' . s')
by A10, FUNCT_1:def 5;
( ex
U0 being
MSAlgebra of
S st
(
U0 = A . i'' &
(Carrier A,s'') . i'' = the
Sorts of
U0 . s'' ) &
rng (F' . s'') c= the
Sorts of
(A . i'') . s'' )
by PRALG_2:def 16;
hence
f . i' in (Carrier A,s'') . i'
by A14, A15;
verum end;
dom (Carrier A,s'') = dom f
by A9, PARTFUN1:def 4;
then
f in product (Carrier A,s'')
by A12, CARD_3:18;
hence
x in the
Sorts of
(product A) . s'
by A8, PRALG_2:def 17;
verum
end; hence
H . s' is
Function of the
Sorts of
U1 . s',the
Sorts of
(product A) . s'
by A3, A4, A5, FUNCT_2:def 1, RELSET_1:11;
verum end;
then reconsider H = H as ManySortedFunction of ,U1 by PBOOLE:def 18;
A16:
H is_homomorphism U1, product A
proof
let o be
OperSymbol of ;
MSUALG_3:def 9 ( 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 s' =
the_result_sort_of o;
A17:
Result o,
U1 = the
Sorts of
U1 . (the_result_sort_of o)
by PRALG_2:10;
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:11;
then A20:
x = {}
by TARSKI:def 1;
A21:
now let i' be
set ;
( i' in I implies ((commute ((commute F) . (the_result_sort_of o))) . (const o,U1)) . i' = (const o,(product A)) . i' )assume
i' in I
;
((commute ((commute F) . (the_result_sort_of o))) . (const o,U1)) . i' = (const o,(product A)) . i'then reconsider ii =
i' as
Element of
I ;
consider F1 being
ManySortedFunction of ,
U1 such that A22:
F1 = F . ii
and A23:
F1 is_homomorphism U1,
A . ii
by A1;
A24:
F1 # x = {}
by A19, A20, Th12;
thus ((commute ((commute F) . (the_result_sort_of o))) . (const o,U1)) . i' =
(F1 . (the_result_sort_of o)) . ((Den o,U1) . x)
by A1, A17, A20, A22, Th28
.=
const o,
(A . ii)
by A23, A24, MSUALG_3:def 9
.=
(const o,(product A)) . i'
by A19, Th10
;
verum end;
const o,
(product A) in Funcs I,
(union { (Result o,(A . i1)) where i1 is Element of I : verum } )
by A19, Th9;
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, Th29;
then dom ((commute ((commute F) . (the_result_sort_of o))) . (const o,U1)) =
dom (Carrier A,(the_result_sort_of o))
by CARD_3:18
.=
I
by PARTFUN1:def 4
;
then A26:
(commute ((commute F) . (the_result_sort_of o))) . (const o,U1) = const o,
(product A)
by A25, A21, FUNCT_1:9;
H # x = {}
by A19, A20, Th12;
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 11
.=
IFEQ (the_arity_of o),
{} ,
(commute (A ?. o)),
(Commute (Frege (A ?. o)))
by PRALG_2:def 20
.=
Commute (Frege (A ?. o))
by A27, FUNCOP_1:def 8
;
then reconsider f1 =
(Den o,(product A)) . (H # x) as
Function by PRALG_2:15;
f1 in rng (Frege (A ?. o))
by A29;
then A31:
dom f1 = I
by PRALG_2:16;
set D =
union { (the Sorts of (A . i') . ss) where i' 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 . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } ))
by Th15;
A33:
now let i' be
set ;
( i' in I implies ((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) . i' = f1 . i' )assume
i' in I
;
((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) . i' = f1 . i'then reconsider ii =
i' as
Element of
I ;
consider F1 being
ManySortedFunction of ,
U1 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, MSUALG_3:def 9;
A37:
now let n be
set ;
( 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 5;
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, Th14
.=
(F1 . s1) . (x . n)
by A38, PARTFUN1:def 8
;
x in Args o,
U1
;
then A40:
x in product (the Sorts of U1 * (the_arity_of o))
by PRALG_2:10;
then A41:
dom x = dom (the Sorts of U1 * (the_arity_of o))
by CARD_3:18;
A42:
dom x =
dom (the Sorts of U1 * (the_arity_of o))
by A40, CARD_3:18
.=
dom (the_arity_of o)
by PRALG_2:10
;
then
x . n in (the Sorts of U1 * (the_arity_of o)) . n
by A38, A40, A41, CARD_3:18;
then A43:
x . n in the
Sorts of
U1 . s1
by A38, A42, A41, FUNCT_1:22;
A44:
(H # x) . n =
(H . ((the_arity_of o) /. n)) . (x . n)
by A38, Th14
.=
(H . s1) . (x . n)
by A38, PARTFUN1:def 8
.=
(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:86
.=
(F1 # x) . n
by A1, A34, A43, A39, A44, Th28
;
verum end;
dom F1 = the
carrier of
S
by PARTFUN1:def 4;
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 . i') . ss) where i' is Element of I, ss is Element of the carrier of S : verum } ))
by A27, A32, FUNCT_6:85;
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 . i') . ss) where i' 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 5;
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 . i') . ss) where i' 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 Th13;
dom (F1 # x) =
dom ((Frege (F1 * (the_arity_of o))) . x)
by MSUALG_3:def 7
.=
dom ((F1 * (the_arity_of o)) .. x)
by A50, PRALG_2:def 8
.=
dom (F1 * (the_arity_of o))
by PRALG_1:def 17
.=
dom (the_arity_of o)
by A45, RELAT_1:46
;
then
F1 # x = (commute (H # x)) . ii
by A49, A37, FUNCT_1:9;
then ((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) . i' =
(Den o,(A . ii)) . ((commute (H # x)) . ii)
by A1, A17, A34, A36, Th28
.=
f1 . i'
by A27, Th23
;
hence
((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) . i' = f1 . i'
;
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, Th29;
then dom ((commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x)) =
dom (Carrier A,(the_result_sort_of o))
by CARD_3:18
.=
I
by PARTFUN1:def 4
;
then
(commute ((commute F) . (the_result_sort_of o))) . ((Den o,U1) . x) = f1
by A31, A33, FUNCT_1:9;
hence
(H . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(product A)) . (H # x)
by A2;
verum 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 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 24
.=
the
carrier of
S /\ (dom H)
by PARTFUN1:def 4
.=
the
carrier of
S /\ the
carrier of
S
by PARTFUN1:def 4
.=
the
carrier of
S
;
A53:
now let s' be
set ;
( s' in the carrier of S implies ((proj A,i) ** H) . s' = F1 . s' )assume
s' in the
carrier of
S
;
((proj A,i) ** H) . s' = F1 . s'then reconsider s1 =
s' as
SortSymbol of ;
A54:
((proj A,i) ** H) . s' =
((proj A,i) . s1) * (H . s1)
by A52, PBOOLE:def 24
.=
(proj (Carrier A,s1),i) * (H . s1)
by Def3
.=
(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 . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
by A1, Th27;
then
commute ((commute F) . s1) in Funcs (the Sorts of U1 . s1),
(Funcs I,(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } ))
by FUNCT_6:85;
then consider f' being
Function such that A55:
f' = commute ((commute F) . s1)
and A56:
dom f' = the
Sorts of
U1 . s1
and
rng f' c= Funcs I,
(union { (the Sorts of (A . i') . s1) where i' is Element of I, s1 is SortSymbol of : verum } )
by FUNCT_2:def 2;
rng f' c= dom (proj (Carrier A,s1),i)
proof
let y be
set ;
TARSKI:def 3 ( not y in rng f' or y in dom (proj (Carrier A,s1),i) )
assume
y in rng f'
;
y in dom (proj (Carrier A,s1),i)
then consider x' being
set such that A57:
x' in dom f'
and A58:
f' . x' = y
by FUNCT_1:def 5;
(commute ((commute F) . s1)) . x' in product (Carrier A,s1)
by A1, A56, A57, Th29;
hence
y in dom (proj (Carrier A,s1),i)
by A55, A58, CARD_3:def 17;
verum
end; then A59:
dom (((proj A,i) ** H) . s') = the
Sorts of
U1 . s'
by A55, A56, A54, RELAT_1:46;
A60:
now let x be
set ;
( x in the Sorts of U1 . s' implies (((proj A,i) ** H) . s') . x = (F1 . s') . x )assume A61:
x in the
Sorts of
U1 . s'
;
(((proj A,i) ** H) . s') . x = (F1 . s') . xthen
(commute ((commute F) . s1)) . x in product (Carrier A,s1)
by A1, Th29;
then A62:
(commute ((commute F) . s1)) . x in dom (proj (Carrier A,s1),i)
by CARD_3:def 17;
thus (((proj A,i) ** H) . s') . x =
(proj (Carrier A,s1),i) . ((commute ((commute F) . s1)) . x)
by A54, A59, A61, FUNCT_1:22
.=
((commute ((commute F) . s1)) . x) . i
by A62, CARD_3:def 17
.=
(F1 . s') . x
by A1, A51, A61, Th28
;
verum end; dom (F1 . s') =
dom (F1 . s1)
.=
the
Sorts of
U1 . s'
by FUNCT_2:def 1
;
hence
((proj A,i) ** H) . s' = F1 . s'
by A59, A60, FUNCT_1:9;
verum end;
dom F1 = the
carrier of
S
by PARTFUN1:def 4;
hence
(proj A,i) ** H = F . i
by A51, A52, A53, FUNCT_1:9;
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