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[ set , set , set ] 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 set st s in the carrier of S holds
for x being set st x in the Sorts of (product A) . s holds
ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
proof
let s be
set ;
( s in the carrier of S implies for x being set st x in the Sorts of (product A) . s holds
ex y being set 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 set st x in the Sorts of (product A) . s holds
ex y being set 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 17;
let x be
set ;
( x in the Sorts of (product A) . s implies ex y being set 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 set 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 4();
A5:
dom (Carrier (product (A / EqR)),s9) = Class EqR
by PARTFUN1:def 4;
A6:
for
a being
set 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
set ;
( 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
A8:
(A / EqR) . a = A | a
by A5, A7, Def5;
reconsider a =
a as non
empty Subset of
I by A5, A7;
A9:
ex
U0 being
MSAlgebra of
S st
(
U0 = (product (A / EqR)) . a &
(Carrier (product (A / EqR)),s9) . a = the
Sorts of
U0 . s9 )
by A5, A7, PRALG_2:def 16;
A10:
dom (A | a) =
(dom A) /\ a
by RELAT_1:90
.=
I /\ a
by PARTFUN1:def 4
.=
a
by XBOOLE_1:28
;
then reconsider Aa1 =
A | a as
ManySortedSet of
a by PARTFUN1:def 4;
for
i being
set st
i in a holds
Aa1 . i is
non-empty MSAlgebra of
S
then reconsider Aa =
Aa1 as
MSAlgebra-Family of
a,
S by PRALG_2:def 12;
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 A5, A7, Def6;
Ji = a
by A5, A7, A13, FUNCT_1:35;
then
(Carrier (product (A / EqR)),s9) . a = product (Carrier Aa,s9)
by A8, A14, A9, PRALG_2:def 17;
hence
y . a in (Carrier (product (A / EqR)),s9) . a
by A4, A5, 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 4
.=
dom y
by PARTFUN1:def 4
;
then
y in product (Carrier (product (A / EqR)),s9)
by A6, CARD_3:18;
hence
(
y in the
Sorts of
(product (product (A / EqR))) . s &
S1[
y,
x,
s] )
by A4, PRALG_2:def 17;
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 set 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 set 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 9 ( 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:10;
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 17;
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
set 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 17
;
A22:
(Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o))
by Th20;
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:11;
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 5;
then reconsider g1 =
(F . (the_result_sort_of o)) . (const o,(product A)) as
Function by A19;
A26:
dom (const o,(product A)) =
dom (Carrier A,(the_result_sort_of o))
by A22, A24, CARD_3:18
.=
I
by PARTFUN1:def 4
;
A27:
now 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 Def6;
A31:
dom ((const o,(product A)) | e) =
I /\ e
by A26, RELAT_1:90
.=
e
by XBOOLE_1:28
;
A32:
now let i1 be
set ;
( 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:90
.=
I /\ e
by PARTFUN1:def 4
.=
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, FUNCT_1:35;
reconsider ii9 =
ii as
Element of
I by A34;
Cs = A | e
by A29, Def5;
then A35:
Cs . ii = A . ii9
by A34, A33, FUNCT_1:70;
thus ((const o,(product A)) | e) . i1 =
(const o,(product A)) . i1
by A31, A34, FUNCT_1:70
.=
const o,
(A . ii9)
by A23, Th10
.=
(const o,(product Cs)) . i1
by A23, A35, Th10
;
verum end;
const o,
(product Cs) in Funcs Ji,
(union { (Result o,(Cs . i9)) where i9 is Element of Ji : verum } )
by A23, Th9;
then dom (const o,(product Cs)) =
Ji
by FUNCT_2:169
.=
e
by A28, FUNCT_1:35
;
hence
(const o,(product A)) | e = const o,
((product (A / EqR)) . e)
by A30, A31, A32, FUNCT_1:9;
verum end; A36:
const o,
(product A) in the
Sorts of
(product A) . (the_result_sort_of o)
by A17, A24, PRALG_2:10;
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, Th9;
then A39:
dom (const o,(product (product (A / EqR)))) = Class EqR
by FUNCT_2:169;
dom g1 =
dom (Carrier (product (A / EqR)),(the_result_sort_of o))
by A19, A25, CARD_3:18
.=
Class EqR
by PARTFUN1:def 4
;
then
(F . (the_result_sort_of o)) . (const o,(product A)) = const o,
(product (product (A / EqR)))
by A39, A37, FUNCT_1:9;
hence
(F . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(product (product (A / EqR)))) . (F # x)
by A23, A24, Th12;
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 Th20;
then reconsider f1 =
(Den o,(product (product (A / EqR)))) . (F # x) as
Function ;
A42:
dom f1 =
dom (Carrier (product (A / EqR)),(the_result_sort_of o))
by A41, CARD_3:18
.=
Class EqR
by PARTFUN1:def 4
;
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 5;
then reconsider g1 =
(F . (the_result_sort_of o)) . ((Den o,(product A)) . x) as
Function by A19;
A44:
now 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 Def6;
A48:
(commute (F # x)) . e is
Element of
Args o,
((product (A / EqR)) . e)
by A40, Th21;
then A49:
(Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e) in product (Carrier Cs,(the_result_sort_of o))
by A47, Th20;
then reconsider f3 =
(Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e) as
Function ;
A50:
now let 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, FUNCT_1:35;
A52:
now let n be
set ;
( 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 5;
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, Th16;
then reconsider f4 =
x . n as
Function ;
A55:
x . n in product (Carrier A,s1)
by A53, A54, PARTFUN1:def 8;
then A56:
x . n in (SORTS A) . s1
by PRALG_2:def 17;
dom f4 =
dom (Carrier A,s1)
by A55, CARD_3:18
.=
I
by PARTFUN1:def 4
;
then A57:
dom (f4 | e) =
I /\ e
by RELAT_1:90
.=
e
by XBOOLE_1:28
;
(F # x) . n in product (Carrier (product (A / EqR)),((the_arity_of o) /. n))
by A53, Th16;
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
set 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, Th14
.=
f7 . (x . n)
by A53, A58, PARTFUN1:def 8
;
then A60:
f5 . e = f4 | e
by A56, A59;
then reconsider f6 =
f5 . e as
Function ;
f6 = ((commute (F # x)) . e) . n
by A53, Th22;
hence ((commute ((commute (F # x)) . e)) . i1) . n =
(f4 | e) . i2
by A47, A48, A53, A60, Th22
.=
f4 . i2
by A51, A57, FUNCT_1:70
.=
((commute x) . i1) . n
by A53, Th22
;
verum end;
(commute x) . i1 is
Element of
Args o,
(A . i1)
by A40, Th21;
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:10;
then A61:
dom ((commute x) . i1) =
dom (the Sorts of (A . i1) * (the_arity_of o))
by CARD_3:18
.=
dom (the_arity_of o)
by PRALG_2:10
;
(commute ((commute (F # x)) . e)) . i2 is
Element of
Args o,
(Cs . i2)
by A40, A47, A48, Th21;
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:10;
then dom ((commute ((commute (F # x)) . e)) . i1) =
dom (the Sorts of (Cs . i2) * (the_arity_of o))
by CARD_3:18
.=
dom (the_arity_of o)
by PRALG_2:10
;
hence
(commute ((commute (F # x)) . e)) . i1 = (commute x) . i1
by A61, A52, FUNCT_1:9;
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 =
dom (Carrier A,(the_result_sort_of o))
by A22, A62, CARD_3:18
.=
I
by PARTFUN1:def 4
;
then A63:
dom (f2 | e) =
I /\ e
by RELAT_1:90
.=
e
by XBOOLE_1:28
;
A64:
(commute (F # x)) . e is
Element of
Args o,
(product Cs)
by A40, A47, Th21;
A65:
now let x1 be
set ;
( x1 in e implies f3 . x1 = (f2 | e) . x1 )A66:
dom (A | e) =
(dom A) /\ e
by RELAT_1:90
.=
I /\ e
by PARTFUN1:def 4
.=
e
by XBOOLE_1:28
;
assume A67:
x1 in e
;
f3 . x1 = (f2 | e) . x1then reconsider i2 =
x1 as
Element of
Ji by A45, FUNCT_1:35;
reconsider i1 =
i2 as
Element of
I by A67;
Cs = A | e
by A46, Def5;
then
Cs . i2 = A . i1
by A67, A66, FUNCT_1:70;
hence f3 . x1 =
(Den o,(A . i1)) . ((commute ((commute (F # x)) . e)) . i2)
by A40, A47, A64, Th23
.=
(Den o,(A . i1)) . ((commute x) . i1)
by A50, A67
.=
f2 . x1
by A40, A62, Th23
.=
(f2 | e) . x1
by A63, A67, FUNCT_1:70
;
verum end; dom f3 =
dom (Carrier Cs,(the_result_sort_of o))
by A49, CARD_3:18
.=
Ji
by PARTFUN1:def 4
.=
e
by A45, FUNCT_1:35
;
hence
f2 | e = (Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e)
by A63, A65, FUNCT_1:9;
verum end; dom g1 =
dom (Carrier (product (A / EqR)),(the_result_sort_of o))
by A19, A43, CARD_3:18
.=
Class EqR
by PARTFUN1:def 4
;
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:9;
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 proj1 F or not F . s = b1 or b1 is one-to-one )let g be
Function;
( not s in proj1 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
dom F = the
carrier of
S
by PARTFUN1:def 4;
then 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
set st
x in the
Sorts of
(product A) . s holds
S1[
f . x,
x,
s]
by A15, A69;
let x1,
x2 be
set ;
FUNCT_1:def 8 ( not x1 in proj1 g or not x2 in proj1 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, PARTFUN1:def 4;
A77:
the
Sorts of
(product A) . s9 = product (Carrier A,s9)
by PRALG_2:def 17;
then A78:
ex
gg being
Function st
(
x1 = gg &
dom gg = dom (Carrier A,s9) & ( for
x9 being
set 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
set 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 4;
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 17;
A82:
for
i being
set st
i in I holds
x1 . i = x2 . i
proof
reconsider f99 =
f . x2 as
Function by A74, A76, A81, Lm1, FUNCT_2:7;
let i be
set ;
( 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 5;
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:28, FUNCT_1:72
.=
x2 . i
by A83, EQREL_1:28, FUNCT_1:72
;
hence
x1 . i = x2 . i
;
verum
end;
dom x1 = I
by A78, PARTFUN1:def 4;
hence
x1 = x2
by A80, A82, FUNCT_1:9;
verum
end;
end;
then A85:
F is_monomorphism product A, product (product (A / EqR))
by A16, MSUALG_3:def 11;
F is "onto"
proof
let s be
set ;
MSUALG_3:def 3 ( not s in the carrier of S or proj2 (F . s) = the Sorts of (product (product (A / EqR))) . s )
assume A86:
s in the
carrier of
S
;
proj2 (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
set 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 17;
for
y being
set holds
(
y in the
Sorts of
(product (product (A / EqR))) . s iff ex
x being
set st
(
x in dom f &
y = f . x ) )
proof
let y be
set ;
( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set 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 17;
then A92:
ex
gg being
Function st
(
y = gg &
dom gg = dom (Carrier (product (A / EqR)),s9) & ( for
x9 being
set 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[
set ,
set ]
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
set st
i in I holds
ex
j being
set st
S2[
i,
j]
proof
let i be
set ;
( i in I implies ex j being set st S2[i,j] )
assume A94:
i in I
;
ex j being set st S2[i,j]
Class EqR,
i in Class EqR
by A94, EQREL_1:def 5;
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 Def6;
ex
U0 being
MSAlgebra of
S st
(
U0 = (product (A / EqR)) . e &
(Carrier (product (A / EqR)),s9) . e = the
Sorts of
U0 . s9 )
by PRALG_2:def 16;
then
(
dom (Carrier (product (A / EqR)),s9) = Class EqR &
(Carrier (product (A / EqR)),s9) . e = product (Carrier Cs,s9) )
by A96, PARTFUN1:def 4, PRALG_2:def 17;
then reconsider y9 =
y . e as
Function by A92, Lm1;
S2[
i,
y9 . i]
by A94, A95, EQREL_1:28;
hence
ex
j being
set st
S2[
i,
j]
;
verum
end;
consider x being
ManySortedSet of
I such that A97:
for
i being
set 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 4;
A99:
for
z being
set st
z in dom (Carrier A,s9) holds
x . z in (Carrier A,s9) . z
proof
let z be
set ;
( 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
by PARTFUN1:def 4;
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:90
.=
I /\ e
by PARTFUN1:def 4
.=
e
by XBOOLE_1:28
;
then A102:
((Carrier A,s9) | e) . z = (Carrier A,s9) . z
by A100, FUNCT_1:70;
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 Def6;
(
Cs = A | e &
Ji = e )
by A103, A104, Def5, FUNCT_1:35;
then A106:
Carrier Cs,
s9 = (Carrier A,s9) | e
by Th2;
ex
U0 being
MSAlgebra of
S st
(
U0 = (product (A / EqR)) . e &
(Carrier (product (A / EqR)),s9) . e = the
Sorts of
U0 . s9 )
by PRALG_2:def 16;
then A107:
(Carrier (product (A / EqR)),s9) . e = product (Carrier Cs,s9)
by A105, PRALG_2:def 17;
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
set 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) =
Ji
by PARTFUN1:def 4
.=
e
by A103, FUNCT_1:35
;
hence
x . z in (Carrier A,s9) . z
by A100, A101, A108, A102, A106;
verum
end;
dom x =
I
by PARTFUN1:def 4
.=
dom (Carrier A,s9)
by PARTFUN1:def 4
;
then A109:
x in the
Sorts of
(product A) . s9
by A89, A99, CARD_3:18;
then A110:
x in dom f
by FUNCT_2:def 1;
then
f . x in rng f
by FUNCT_1:def 5;
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 17;
then reconsider f9 =
f . x as
Function ;
A112:
for
e being
set st
e in Class EqR holds
y . e = f9 . e
proof
let e be
set ;
( 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 Def6;
ex
U0 being
MSAlgebra of
S st
(
U0 = (product (A / EqR)) . e &
(Carrier (product (A / EqR)),s9) . e = the
Sorts of
U0 . s9 )
by PRALG_2:def 16;
then A115:
(Carrier (product (A / EqR)),s9) . e = product (Carrier Cs,s9)
by A114, PRALG_2:def 17;
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:90
.=
I /\ e
by PARTFUN1:def 4
.=
e
by XBOOLE_1:28
;
A118:
for
i being
set 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
set 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 =
Ji
by PARTFUN1:def 4
.=
e
by A113, FUNCT_1:35
;
then
x | e = y9
by A117, A118, FUNCT_1:def 17;
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
set 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, A98, A112, FUNCT_1:def 17;
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
set st
(
x in dom f &
y = f . x ) )
by A90;
verum
end;
hence
proj2 (F . s) = the
Sorts of
(product (product (A / EqR))) . s
by A87, FUNCT_1:def 5;
verum
end;
then
F is_epimorphism product A, product (product (A / EqR))
by A16, MSUALG_3:def 10;
then
F is_isomorphism product A, product (product (A / EqR))
by A85, MSUALG_3:def 12;
hence
product A, product (product (A / EqR)) are_isomorphic
by MSUALG_3:def 13; verum