let I be non empty set ; for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let S be non empty non void ManySortedSign ; for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let A be MSAlgebra-Family of I,S; for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let EqR be Equivalence_Relation of I; product A, product (product (A / EqR)) are_isomorphic
set U1 = product A;
set U2 = product (product (A / EqR));
set U19 = the Sorts of (product A);
set U29 = the Sorts of (product (product (A / EqR)));
defpred S1[ object , object , object ] means for f1, g1 being Function st f1 = $2 & g1 = $1 holds
for e being Element of Class EqR holds g1 . e = f1 | e;
A1:
for s being object st s in the carrier of S holds
for x being object st x in the Sorts of (product A) . s holds
ex y being object st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
proof
let s be
object ;
( s in the carrier of S implies for x being object st x in the Sorts of (product A) . s holds
ex y being object st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) )
assume
s in the
carrier of
S
;
for x being object st x in the Sorts of (product A) . s holds
ex y being object st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
then reconsider s9 =
s as
SortSymbol of
S ;
A2:
the
Sorts of
(product A) . s9 = product (Carrier (A,s9))
by PRALG_2:def 10;
let x be
object ;
( x in the Sorts of (product A) . s implies ex y being object st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) )
assume A3:
x in the
Sorts of
(product A) . s
;
ex y being object st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
reconsider x =
x as
Function by A3, A2;
deffunc H1(
set )
-> set =
x | $1;
consider y being
ManySortedSet of
Class EqR such that A4:
for
c being
set st
c in Class EqR holds
y . c = H1(
c)
from PBOOLE:sch 7();
A5:
dom (Carrier ((product (A / EqR)),s9)) = Class EqR
by PARTFUN1:def 2;
A6:
for
a being
object st
a in dom (Carrier ((product (A / EqR)),s9)) holds
y . a in (Carrier ((product (A / EqR)),s9)) . a
proof
set A9 =
product (A / EqR);
let a be
object ;
( a in dom (Carrier ((product (A / EqR)),s9)) implies y . a in (Carrier ((product (A / EqR)),s9)) . a )
assume A7:
a in dom (Carrier ((product (A / EqR)),s9))
;
y . a in (Carrier ((product (A / EqR)),s9)) . a
reconsider a =
a as
set by TARSKI:1;
A8:
(A / EqR) . a = A | a
by A7, Def4;
reconsider a =
a as non
empty Subset of
I by A5, A7;
A9:
ex
U0 being
MSAlgebra over
S st
(
U0 = (product (A / EqR)) . a &
(Carrier ((product (A / EqR)),s9)) . a = the
Sorts of
U0 . s9 )
by A7, PRALG_2:def 9;
A10:
dom (A | a) =
(dom A) /\ a
by RELAT_1:61
.=
I /\ a
by PARTFUN1:def 2
.=
a
by XBOOLE_1:28
;
then reconsider Aa1 =
A | a as
ManySortedSet of
a by PARTFUN1:def 2;
for
i being
object st
i in a holds
Aa1 . i is
non-empty MSAlgebra over
S
then reconsider Aa =
Aa1 as
MSAlgebra-Family of
a,
S by PRALG_2:def 5;
x | a in product ((Carrier (A,s9)) | a)
by A3, A2, Th1;
then A12:
x | a in product (Carrier (Aa,s9))
by Th2;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A13:
Ji = (id (Class EqR)) . a
and A14:
(
Cs = (A / EqR) . a &
(product (A / EqR)) . a = product Cs )
by A7, Def5;
Ji = a
by A7, A13, FUNCT_1:18;
then
(Carrier ((product (A / EqR)),s9)) . a = product (Carrier (Aa,s9))
by A8, A14, A9, PRALG_2:def 10;
hence
y . a in (Carrier ((product (A / EqR)),s9)) . a
by A4, A7, A12;
verum
end;
take
y
;
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
dom (Carrier ((product (A / EqR)),s9)) =
Class EqR
by PARTFUN1:def 2
.=
dom y
by PARTFUN1:def 2
;
then
y in product (Carrier ((product (A / EqR)),s9))
by A6, CARD_3:9;
hence
(
y in the
Sorts of
(product (product (A / EqR))) . s &
S1[
y,
x,
s] )
by A4, PRALG_2:def 10;
verum
end;
consider F being ManySortedFunction of the Sorts of (product A), the Sorts of (product (product (A / EqR))) such that
A15:
for s being object st s in the carrier of S holds
ex f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) st
( f = F . s & ( for x being object st x in the Sorts of (product A) . s holds
S1[f . x,x,s] ) )
from MSSUBFAM:sch 1(A1);
A16:
F is_homomorphism product A, product (product (A / EqR))
proof
let o be
OperSymbol of
S;
MSUALG_3:def 7 ( Args (o,(product A)) = {} or for b1 being Element of Args (o,(product A)) holds (F . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(product (product (A / EqR))))) . (F # b1) )
assume
Args (
o,
(product A))
<> {}
;
for b1 being Element of Args (o,(product A)) holds (F . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(product (product (A / EqR))))) . (F # b1)
let x be
Element of
Args (
o,
(product A));
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
thus
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
verumproof
A17:
(Den (o,(product A))) . x in Result (
o,
(product A))
;
then A18:
(Den (o,(product A))) . x in the
Sorts of
(product A) . (the_result_sort_of o)
by PRALG_2:3;
set s =
the_result_sort_of o;
set U3 =
product (A / EqR);
A19:
the
Sorts of
(product (product (A / EqR))) . (the_result_sort_of o) = product (Carrier ((product (A / EqR)),(the_result_sort_of o)))
by PRALG_2:def 10;
A20:
ex
f being
Function of
( the Sorts of (product A) . (the_result_sort_of o)),
( the Sorts of (product (product (A / EqR))) . (the_result_sort_of o)) st
(
f = F . (the_result_sort_of o) & ( for
x9 being
object st
x9 in the
Sorts of
(product A) . (the_result_sort_of o) holds
S1[
f . x9,
x9,
the_result_sort_of o] ) )
by A15;
A21:
dom (F . (the_result_sort_of o)) =
(SORTS A) . (the_result_sort_of o)
by FUNCT_2:def 1
.=
product (Carrier (A,(the_result_sort_of o)))
by PRALG_2:def 10
;
A22:
(Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
by Th19;
per cases
( the_arity_of o = {} or the_arity_of o <> {} )
;
suppose A23:
the_arity_of o = {}
;
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)then
Args (
o,
(product A))
= {{}}
by PRALG_2:4;
then A24:
x = {}
by TARSKI:def 1;
then A25:
(F . (the_result_sort_of o)) . (const (o,(product A))) in rng (F . (the_result_sort_of o))
by A21, A22, FUNCT_1:def 3;
reconsider g1 =
(F . (the_result_sort_of o)) . (const (o,(product A))) as
Function by A19;
A26:
dom (const (o,(product A))) = I
by PARTFUN1:def 2, A22, A24;
A27:
now for e being Element of Class EqR holds (const (o,(product A))) | e = const (o,((product (A / EqR)) . e))let e be
Element of
Class EqR;
(const (o,(product A))) | e = const (o,((product (A / EqR)) . e))consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A28:
Ji = (id (Class EqR)) . e
and A29:
Cs = (A / EqR) . e
and A30:
(product (A / EqR)) . e = product Cs
by Def5;
A31:
dom ((const (o,(product A))) | e) =
I /\ e
by A26, RELAT_1:61
.=
e
by XBOOLE_1:28
;
A32:
now for i1 being object st i1 in e holds
((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1let i1 be
object ;
( i1 in e implies ((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1 )A33:
dom (A | e) =
(dom A) /\ e
by RELAT_1:61
.=
I /\ e
by PARTFUN1:def 2
.=
e
by XBOOLE_1:28
;
assume A34:
i1 in e
;
((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1then reconsider ii =
i1 as
Element of
Ji by A28;
reconsider ii9 =
ii as
Element of
I by A34;
Cs = A | e
by A29, Def4;
then A35:
Cs . ii = A . ii9
by A34, A33, FUNCT_1:47;
thus ((const (o,(product A))) | e) . i1 =
(const (o,(product A))) . i1
by A31, A34, FUNCT_1:47
.=
const (
o,
(A . ii9))
by A23, Th9
.=
(const (o,(product Cs))) . i1
by A23, A35, Th9
;
verum end;
const (
o,
(product Cs))
in Funcs (
Ji,
(union { (Result (o,(Cs . i9))) where i9 is Element of Ji : verum } ))
by A23, Th8;
then
dom (const (o,(product Cs))) = e
by A28, FUNCT_2:92;
hence
(const (o,(product A))) | e = const (
o,
((product (A / EqR)) . e))
by A30, A31, A32, FUNCT_1:2;
verum end; A36:
const (
o,
(product A))
in the
Sorts of
(product A) . (the_result_sort_of o)
by A17, A24, PRALG_2:3;
const (
o,
(product (product (A / EqR))))
in Funcs (
(Class EqR),
(union { (Result (o,((product (A / EqR)) . i9))) where i9 is Element of Class EqR : verum } ))
by A23, Th8;
then A39:
dom (const (o,(product (product (A / EqR))))) = Class EqR
by FUNCT_2:92;
dom g1 = Class EqR
by PARTFUN1:def 2, A19, A25;
then
(F . (the_result_sort_of o)) . (const (o,(product A))) = const (
o,
(product (product (A / EqR))))
by A39, A37, FUNCT_1:2;
hence
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
by A23, A24, Th11;
verum end; suppose A40:
the_arity_of o <> {}
;
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)A41:
(Den (o,(product (product (A / EqR))))) . (F # x) in product (Carrier ((product (A / EqR)),(the_result_sort_of o)))
by Th19;
then reconsider f1 =
(Den (o,(product (product (A / EqR))))) . (F # x) as
Function ;
A42:
dom f1 = Class EqR
by PARTFUN1:def 2, A41;
A43:
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) in rng (F . (the_result_sort_of o))
by A21, A22, FUNCT_1:def 3;
reconsider g1 =
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) as
Function by A19;
A44:
now for e being Element of Class EqR
for f2 being Function st f2 = (Den (o,(product A))) . x holds
f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e)let e be
Element of
Class EqR;
for f2 being Function st f2 = (Den (o,(product A))) . x holds
f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e)consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A45:
Ji = (id (Class EqR)) . e
and A46:
Cs = (A / EqR) . e
and A47:
(product (A / EqR)) . e = product Cs
by Def5;
A48:
(commute (F # x)) . e is
Element of
Args (
o,
((product (A / EqR)) . e))
by A40, Th20;
then A49:
(Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) in product (Carrier (Cs,(the_result_sort_of o)))
by A47, Th19;
then reconsider f3 =
(Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) as
Function ;
A50:
now for i1 being Element of I st i1 in e holds
(commute ((commute (F # x)) . e)) . i1 = (commute x) . i1let i1 be
Element of
I;
( i1 in e implies (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 )assume A51:
i1 in e
;
(commute ((commute (F # x)) . e)) . i1 = (commute x) . i1then reconsider i2 =
i1 as
Element of
Ji by A45;
A52:
now for n being object st n in dom (the_arity_of o) holds
((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . nlet n be
object ;
( n in dom (the_arity_of o) implies ((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . n )assume A53:
n in dom (the_arity_of o)
;
((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . 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
SortSymbol of
S ;
A54:
x . n in product (Carrier (A,((the_arity_of o) /. n)))
by A53, Th15;
then reconsider f4 =
x . n as
Function ;
A55:
x . n in product (Carrier (A,s1))
by A53, A54, PARTFUN1:def 6;
then A56:
x . n in (SORTS A) . s1
by PRALG_2:def 10;
dom f4 = I
by PARTFUN1:def 2, A55;
then A57:
dom (f4 | e) =
I /\ e
by RELAT_1:61
.=
e
by XBOOLE_1:28
;
(F # x) . n in product (Carrier ((product (A / EqR)),((the_arity_of o) /. n)))
by A53, Th15;
then reconsider f5 =
(F # x) . n as
Function ;
consider f7 being
Function of
( the Sorts of (product A) . s1),
( the Sorts of (product (product (A / EqR))) . s1) such that A58:
f7 = F . s1
and A59:
for
x9 being
object st
x9 in the
Sorts of
(product A) . s1 holds
S1[
f7 . x9,
x9,
s1]
by A15;
f5 =
(F . ((the_arity_of o) /. n)) . (x . n)
by A53, Th13
.=
f7 . (x . n)
by A53, A58, PARTFUN1:def 6
;
then A60:
f5 . e = f4 | e
by A56, A59;
then reconsider f6 =
f5 . e as
Function ;
f6 = ((commute (F # x)) . e) . n
by A53, Th21;
hence ((commute ((commute (F # x)) . e)) . i1) . n =
(f4 | e) . i2
by A47, A48, A53, A60, Th21
.=
f4 . i2
by A51, A57, FUNCT_1:47
.=
((commute x) . i1) . n
by A53, Th21
;
verum end;
(commute x) . i1 is
Element of
Args (
o,
(A . i1))
by A40, Th20;
then
(commute x) . i1 in Args (
o,
(A . i1))
;
then
(commute x) . i1 in product ( the Sorts of (A . i1) * (the_arity_of o))
by PRALG_2:3;
then A61:
dom ((commute x) . i1) =
dom ( the Sorts of (A . i1) * (the_arity_of o))
by CARD_3:9
.=
dom (the_arity_of o)
by PRALG_2:3
;
(commute ((commute (F # x)) . e)) . i2 is
Element of
Args (
o,
(Cs . i2))
by A40, A47, A48, Th20;
then
(commute ((commute (F # x)) . e)) . i2 in Args (
o,
(Cs . i2))
;
then
(commute ((commute (F # x)) . e)) . i2 in product ( the Sorts of (Cs . i2) * (the_arity_of o))
by PRALG_2:3;
then dom ((commute ((commute (F # x)) . e)) . i1) =
dom ( the Sorts of (Cs . i2) * (the_arity_of o))
by CARD_3:9
.=
dom (the_arity_of o)
by PRALG_2:3
;
hence
(commute ((commute (F # x)) . e)) . i1 = (commute x) . i1
by A61, A52;
verum end; let f2 be
Function;
( f2 = (Den (o,(product A))) . x implies f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) )assume A62:
f2 = (Den (o,(product A))) . x
;
f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e)
dom f2 = I
by PARTFUN1:def 2, A22, A62;
then A63:
dom (f2 | e) =
I /\ e
by RELAT_1:61
.=
e
by XBOOLE_1:28
;
A64:
(commute (F # x)) . e is
Element of
Args (
o,
(product Cs))
by A40, A47, Th20;
A65:
now for x1 being object st x1 in e holds
f3 . x1 = (f2 | e) . x1let x1 be
object ;
( x1 in e implies f3 . x1 = (f2 | e) . x1 )A66:
dom (A | e) =
(dom A) /\ e
by RELAT_1:61
.=
I /\ e
by PARTFUN1:def 2
.=
e
by XBOOLE_1:28
;
assume A67:
x1 in e
;
f3 . x1 = (f2 | e) . x1then reconsider i2 =
x1 as
Element of
Ji by A45;
reconsider i1 =
i2 as
Element of
I by A67;
Cs = A | e
by A46, Def4;
then
Cs . i2 = A . i1
by A67, A66, FUNCT_1:47;
hence f3 . x1 =
(Den (o,(A . i1))) . ((commute ((commute (F # x)) . e)) . i2)
by A40, A47, A64, Th22
.=
(Den (o,(A . i1))) . ((commute x) . i1)
by A50, A67
.=
f2 . x1
by A40, A62, Th22
.=
(f2 | e) . x1
by A63, A67, FUNCT_1:47
;
verum end; dom f3 =
dom (Carrier (Cs,(the_result_sort_of o)))
by A49, CARD_3:9
.=
e
by A45, PARTFUN1:def 2
;
hence
f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e)
by A63, A65, FUNCT_1:2;
verum end;
dom g1 = Class EqR
by PARTFUN1:def 2, A19, A43;
hence
(F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x)
by A42, A68, FUNCT_1:2;
verum end;
end;
end;
F is "1-1"
proof
let s be
set ;
MSUALG_3:def 2 for b1 being set holds
( not s in dom F or not F . s = b1 or b1 is one-to-one )let g be
Function;
( not s in dom F or not F . s = g or g is one-to-one )
assume that A69:
s in dom F
and A70:
F . s = g
;
g is one-to-one
consider f being
Function of
( the Sorts of (product A) . s),
( the Sorts of (product (product (A / EqR))) . s) such that A71:
f = F . s
and A72:
for
x being
object st
x in the
Sorts of
(product A) . s holds
S1[
f . x,
x,
s]
by A15, A69;
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom g or not x2 in dom g or not g . x1 = g . x2 or x1 = x2 )
assume that A73:
x1 in dom g
and A74:
x2 in dom g
and A75:
g . x1 = g . x2
;
x1 = x2
A76:
dom f = dom g
by A70, A71;
thus
x1 = x2
verumproof
reconsider s9 =
s as
SortSymbol of
S by A69;
A77:
the
Sorts of
(product A) . s9 = product (Carrier (A,s9))
by PRALG_2:def 10;
then A78:
ex
gg being
Function st
(
x1 = gg &
dom gg = dom (Carrier (A,s9)) & ( for
x9 being
object st
x9 in dom (Carrier (A,s9)) holds
gg . x9 in (Carrier (A,s9)) . x9 ) )
by A73, A76, CARD_3:def 5;
A79:
ex
gg1 being
Function st
(
x2 = gg1 &
dom gg1 = dom (Carrier (A,s9)) & ( for
x9 being
object st
x9 in dom (Carrier (A,s9)) holds
gg1 . x9 in (Carrier (A,s9)) . x9 ) )
by A74, A76, A77, CARD_3:def 5;
reconsider x2 =
x2 as
Function by A74, A76, A77;
A80:
dom x2 = I
by A79, PARTFUN1:def 2;
reconsider x1 =
x1 as
Function by A73, A76, A77;
A81:
the
Sorts of
(product (product (A / EqR))) . s = product (Carrier ((product (A / EqR)),s9))
by PRALG_2:def 10;
A82:
for
i being
object st
i in I holds
x1 . i = x2 . i
proof
reconsider f99 =
f . x2 as
Function by A81;
let i be
object ;
( i in I implies x1 . i = x2 . i )
assume A83:
i in I
;
x1 . i = x2 . i
then A84:
Class (
EqR,
i) is
Element of
Class EqR
by EQREL_1:def 3;
then x1 | (Class (EqR,i)) =
f99 . (Class (EqR,i))
by A70, A73, A75, A71, A72, A76
.=
x2 | (Class (EqR,i))
by A74, A72, A76, A84
;
then x1 . i =
(x2 | (Class (EqR,i))) . i
by A83, EQREL_1:20, FUNCT_1:49
.=
x2 . i
by A83, EQREL_1:20, FUNCT_1:49
;
hence
x1 . i = x2 . i
;
verum
end;
dom x1 = I
by A78, PARTFUN1:def 2;
hence
x1 = x2
by A80, A82, FUNCT_1:2;
verum
end;
end;
then A85:
F is_monomorphism product A, product (product (A / EqR))
by A16;
F is "onto"
proof
let s be
set ;
MSUALG_3:def 3 ( not s in the carrier of S or rng (F . s) = the Sorts of (product (product (A / EqR))) . s )
assume A86:
s in the
carrier of
S
;
rng (F . s) = the Sorts of (product (product (A / EqR))) . s
reconsider s9 =
s as
SortSymbol of
S by A86;
consider f being
Function of
( the Sorts of (product A) . s),
( the Sorts of (product (product (A / EqR))) . s) such that A87:
f = F . s
and A88:
for
x being
object st
x in the
Sorts of
(product A) . s holds
S1[
f . x,
x,
s]
by A15, A86;
A89:
the
Sorts of
(product A) . s9 = product (Carrier (A,s9))
by PRALG_2:def 10;
for
y being
object holds
(
y in the
Sorts of
(product (product (A / EqR))) . s iff ex
x being
object st
(
x in dom f &
y = f . x ) )
proof
let y be
object ;
( y in the Sorts of (product (product (A / EqR))) . s iff ex x being object st
( x in dom f & y = f . x ) )
A90:
(
y in the
Sorts of
(product (product (A / EqR))) . s implies ex
x being
set st
(
x in dom f &
y = f . x ) )
proof
assume
y in the
Sorts of
(product (product (A / EqR))) . s
;
ex x being set st
( x in dom f & y = f . x )
then A91:
y in product (Carrier ((product (A / EqR)),s9))
by PRALG_2:def 10;
then A92:
ex
gg being
Function st
(
y = gg &
dom gg = dom (Carrier ((product (A / EqR)),s9)) & ( for
x9 being
object st
x9 in dom (Carrier ((product (A / EqR)),s9)) holds
gg . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) )
by CARD_3:def 5;
reconsider y =
y as
Function by A91;
defpred S2[
object ,
object ]
means ex
e being
Element of
Class EqR ex
f being
Function st
( $1
in e &
f = y . e & $2
= f . $1 );
A93:
for
i being
object st
i in I holds
ex
j being
object st
S2[
i,
j]
proof
let i be
object ;
( i in I implies ex j being object st S2[i,j] )
assume A94:
i in I
;
ex j being object st S2[i,j]
Class (
EqR,
i)
in Class EqR
by A94, EQREL_1:def 3;
then consider e being
Element of
Class EqR such that A95:
e = Class (
EqR,
i)
;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that
Ji = (id (Class EqR)) . e
and
Cs = (A / EqR) . e
and A96:
(product (A / EqR)) . e = product Cs
by Def5;
ex
U0 being
MSAlgebra over
S st
(
U0 = (product (A / EqR)) . e &
(Carrier ((product (A / EqR)),s9)) . e = the
Sorts of
U0 . s9 )
by PRALG_2:def 9;
then
(
dom (Carrier ((product (A / EqR)),s9)) = Class EqR &
(Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) )
by A96, PARTFUN1:def 2, PRALG_2:def 10;
then reconsider y9 =
y . e as
Function by A92, Lm1;
S2[
i,
y9 . i]
by A94, A95, EQREL_1:20;
hence
ex
j being
object st
S2[
i,
j]
;
verum
end;
consider x being
ManySortedSet of
I such that A97:
for
i being
object st
i in I holds
S2[
i,
x . i]
from PBOOLE:sch 3(A93);
A98:
dom (Carrier ((product (A / EqR)),s9)) = Class EqR
by PARTFUN1:def 2;
A99:
for
z being
object st
z in dom (Carrier (A,s9)) holds
x . z in (Carrier (A,s9)) . z
proof
let z be
object ;
( z in dom (Carrier (A,s9)) implies x . z in (Carrier (A,s9)) . z )
assume
z in dom (Carrier (A,s9))
;
x . z in (Carrier (A,s9)) . z
then
z in I
;
then consider e being
Element of
Class EqR,
f1 being
Function such that A100:
z in e
and A101:
(
f1 = y . e &
x . z = f1 . z )
by A97;
dom ((Carrier (A,s9)) | e) =
(dom (Carrier (A,s9))) /\ e
by RELAT_1:61
.=
I /\ e
by PARTFUN1:def 2
.=
e
by XBOOLE_1:28
;
then A102:
((Carrier (A,s9)) | e) . z = (Carrier (A,s9)) . z
by A100, FUNCT_1:47;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A103:
Ji = (id (Class EqR)) . e
and A104:
Cs = (A / EqR) . e
and A105:
(product (A / EqR)) . e = product Cs
by Def5;
(
Cs = A | e &
Ji = e )
by A103, A104, Def4;
then A106:
Carrier (
Cs,
s9)
= (Carrier (A,s9)) | e
by Th2;
ex
U0 being
MSAlgebra over
S st
(
U0 = (product (A / EqR)) . e &
(Carrier ((product (A / EqR)),s9)) . e = the
Sorts of
U0 . s9 )
by PRALG_2:def 9;
then A107:
(Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9))
by A105, PRALG_2:def 10;
y . e in (Carrier ((product (A / EqR)),s9)) . e
by A92, A98;
then A108:
ex
g being
Function st
(
y . e = g &
dom g = dom (Carrier (Cs,s9)) & ( for
x9 being
object st
x9 in dom (Carrier (Cs,s9)) holds
g . x9 in (Carrier (Cs,s9)) . x9 ) )
by A107, CARD_3:def 5;
dom (Carrier (Cs,s9)) = e
by A103, PARTFUN1:def 2;
hence
x . z in (Carrier (A,s9)) . z
by A100, A101, A108, A102, A106;
verum
end;
dom x =
I
by PARTFUN1:def 2
.=
dom (Carrier (A,s9))
by PARTFUN1:def 2
;
then A109:
x in the
Sorts of
(product A) . s9
by A89, A99, CARD_3:9;
then A110:
x in dom f
by FUNCT_2:def 1;
then
f . x in rng f
by FUNCT_1:def 3;
then
f . x in the
Sorts of
(product (product (A / EqR))) . s
;
then A111:
f . x in product (Carrier ((product (A / EqR)),s9))
by PRALG_2:def 10;
then reconsider f9 =
f . x as
Function ;
A112:
for
e being
object st
e in Class EqR holds
y . e = f9 . e
proof
let e be
object ;
( e in Class EqR implies y . e = f9 . e )
assume
e in Class EqR
;
y . e = f9 . e
then reconsider e =
e as
Element of
Class EqR ;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A113:
Ji = (id (Class EqR)) . e
and
Cs = (A / EqR) . e
and A114:
(product (A / EqR)) . e = product Cs
by Def5;
ex
U0 being
MSAlgebra over
S st
(
U0 = (product (A / EqR)) . e &
(Carrier ((product (A / EqR)),s9)) . e = the
Sorts of
U0 . s9 )
by PRALG_2:def 9;
then A115:
(Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9))
by A114, PRALG_2:def 10;
A116:
y . e in (Carrier ((product (A / EqR)),s9)) . e
by A92, A98;
then reconsider y9 =
y . e as
Function by A115;
A117:
dom (x | e) =
(dom x) /\ e
by RELAT_1:61
.=
I /\ e
by PARTFUN1:def 2
.=
e
by XBOOLE_1:28
;
A118:
for
i being
object st
i in e holds
(x | e) . i = y9 . i
ex
g being
Function st
(
y . e = g &
dom g = dom (Carrier (Cs,s9)) & ( for
x9 being
object st
x9 in dom (Carrier (Cs,s9)) holds
g . x9 in (Carrier (Cs,s9)) . x9 ) )
by A116, A115, CARD_3:def 5;
then
dom y9 = e
by A113, PARTFUN1:def 2;
then
x | e = y9
by A117, A118;
hence
y . e = f9 . e
by A88, A109;
verum
end;
ex
gg9 being
Function st
(
f . x = gg9 &
dom gg9 = dom (Carrier ((product (A / EqR)),s9)) & ( for
x9 being
object st
x9 in dom (Carrier ((product (A / EqR)),s9)) holds
gg9 . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) )
by A111, CARD_3:def 5;
then
y = f9
by A92, A112;
hence
ex
x being
set st
(
x in dom f &
y = f . x )
by A110;
verum
end;
( ex
x being
set st
(
x in dom f &
y = f . x ) implies
y in the
Sorts of
(product (product (A / EqR))) . s )
hence
(
y in the
Sorts of
(product (product (A / EqR))) . s iff ex
x being
object st
(
x in dom f &
y = f . x ) )
by A90;
verum
end;
hence
rng (F . s) = the
Sorts of
(product (product (A / EqR))) . s
by A87, FUNCT_1:def 3;
verum
end;
then
F is_epimorphism product A, product (product (A / EqR))
by A16;
then
F is_isomorphism product A, product (product (A / EqR))
by A85;
hence
product A, product (product (A / EqR)) are_isomorphic
; verum