let I be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
let EqR be Equivalence_Relation of I; :: thesis: product A, product (product (A / EqR)) are_isomorphic
set U1 = product A;
set U2 = product (product (A / EqR));
set U1' = the Sorts of (product A);
set U2' = 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 ;
:: thesis: ( 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 A2:
s in the
carrier of
S
;
:: thesis: 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] )
let x be
set ;
:: thesis: ( 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
;
:: thesis: ex y being set st
( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
reconsider s' =
s as
SortSymbol of
S by A2;
A4:
the
Sorts of
(product A) . s' = product (Carrier A,s')
by PRALG_2:def 17;
then reconsider x =
x as
Function by A3;
deffunc H1(
set )
-> set =
x | $1;
consider y being
ManySortedSet of
such that A5:
for
c being
set st
c in Class EqR holds
y . c = H1(
c)
from PBOOLE:sch 4();
take
y
;
:: thesis: ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] )
y in product (Carrier (product (A / EqR)),s')
proof
A6:
dom (Carrier (product (A / EqR)),s') =
Class EqR
by PARTFUN1:def 4
.=
dom y
by PARTFUN1:def 4
;
A7:
dom (Carrier (product (A / EqR)),s') = Class EqR
by PARTFUN1:def 4;
for
a being
set st
a in dom (Carrier (product (A / EqR)),s') holds
y . a in (Carrier (product (A / EqR)),s') . a
proof
let a be
set ;
:: thesis: ( a in dom (Carrier (product (A / EqR)),s') implies y . a in (Carrier (product (A / EqR)),s') . a )
assume A8:
a in dom (Carrier (product (A / EqR)),s')
;
:: thesis: y . a in (Carrier (product (A / EqR)),s') . a
set A' =
product (A / EqR);
A9:
(A / EqR) . a = A | a
by A7, A8, Def5;
consider b being
set such that A10:
b in I
and A11:
a = Class EqR,
b
by A7, A8, EQREL_1:def 5;
reconsider a =
a as non
empty Subset of
I by A10, A11, EQREL_1:28;
A12:
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
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,s') | a)
by A3, A4, Th1;
then A14:
x | a in product (Carrier Aa,s')
by Th2;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A15:
Ji = (id (Class EqR)) . a
and A16:
Cs = (A / EqR) . a
and A17:
(product (A / EqR)) . a = product Cs
by A7, A8, Def6;
A18:
Ji = a
by A7, A8, A15, FUNCT_1:35;
consider U0 being
MSAlgebra of
S such that A19:
(
U0 = (product (A / EqR)) . a &
(Carrier (product (A / EqR)),s') . a = the
Sorts of
U0 . s' )
by A7, A8, PRALG_2:def 16;
(Carrier (product (A / EqR)),s') . a = product (Carrier Aa,s')
by A9, A16, A17, A18, A19, PRALG_2:def 17;
hence
y . a in (Carrier (product (A / EqR)),s') . a
by A5, A7, A8, A14;
:: thesis: verum
end;
hence
y in product (Carrier (product (A / EqR)),s')
by A6, CARD_3:18;
:: thesis: verum
end;
hence
(
y in the
Sorts of
(product (product (A / EqR))) . s &
S1[
y,
x,
s] )
by A5, PRALG_2:def 17;
:: thesis: verum
end;
consider F being ManySortedFunction of the Sorts of (product A),the Sorts of (product (product (A / EqR))) such that
A20:
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);
A21:
F is_homomorphism product A, product (product (A / EqR))
proof
let o be
OperSymbol of
S;
:: according to MSUALG_3:def 9 :: thesis: ( 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) <> {}
;
:: thesis: 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);
:: thesis: (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)
:: thesis: verumproof
set s =
the_result_sort_of o;
set U3 =
product (A / EqR);
consider 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)) such that A22:
f = F . (the_result_sort_of o)
and A23:
for
x' being
set st
x' in the
Sorts of
(product A) . (the_result_sort_of o) holds
S1[
f . x',
x',
the_result_sort_of o]
by A20;
A24:
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;
A25:
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
;
A26:
(Den o,(product A)) . x in Result o,
(product A)
;
then A27:
(Den o,(product A)) . x in the
Sorts of
(product A) . (the_result_sort_of o)
by PRALG_2:10;
A28:
(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 A29:
the_arity_of o = {}
;
:: thesis: (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 A30:
x = {}
by TARSKI:def 1;
then A31:
const o,
(product A) in the
Sorts of
(product A) . (the_result_sort_of o)
by A26, PRALG_2:10;
A32:
dom (const o,(product A)) =
dom (Carrier A,(the_result_sort_of o))
by A28, A30, CARD_3:18
.=
I
by PARTFUN1:def 4
;
A33:
(F . (the_result_sort_of o)) . (const o,(product A)) in rng (F . (the_result_sort_of o))
by A25, A28, A30, FUNCT_1:def 5;
then reconsider g1 =
(F . (the_result_sort_of o)) . (const o,(product A)) as
Function by A24;
A34:
dom g1 =
dom (Carrier (product (A / EqR)),(the_result_sort_of o))
by A24, A33, CARD_3:18
.=
Class EqR
by PARTFUN1:def 4
;
const o,
(product (product (A / EqR))) in Funcs (Class EqR),
(union { (Result o,((product (A / EqR)) . i')) where i' is Element of Class EqR : verum } )
by A29, Th9;
then A35:
dom (const o,(product (product (A / EqR)))) = Class EqR
by FUNCT_2:169;
A36:
now let e be
Element of
Class EqR;
:: thesis: (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 A37:
(
Ji = (id (Class EqR)) . e &
Cs = (A / EqR) . e &
(product (A / EqR)) . e = product Cs )
by Def6;
A38:
dom ((const o,(product A)) | e) =
I /\ e
by A32, RELAT_1:90
.=
e
by XBOOLE_1:28
;
const o,
(product Cs) in Funcs Ji,
(union { (Result o,(Cs . i')) where i' is Element of Ji : verum } )
by A29, Th9;
then A39:
dom (const o,(product Cs)) =
Ji
by FUNCT_2:169
.=
e
by A37, FUNCT_1:35
;
now let i1 be
set ;
:: thesis: ( i1 in e implies ((const o,(product A)) | e) . i1 = (const o,(product Cs)) . i1 )assume A40:
i1 in e
;
:: thesis: ((const o,(product A)) | e) . i1 = (const o,(product Cs)) . i1then reconsider ii =
i1 as
Element of
Ji by A37, FUNCT_1:35;
reconsider ii' =
ii as
Element of
I by A40;
A41:
dom (A | e) =
(dom A) /\ e
by RELAT_1:90
.=
I /\ e
by PARTFUN1:def 4
.=
e
by XBOOLE_1:28
;
Cs = A | e
by A37, Def5;
then A42:
Cs . ii = A . ii'
by A40, A41, FUNCT_1:70;
thus ((const o,(product A)) | e) . i1 =
(const o,(product A)) . i1
by A38, A40, FUNCT_1:70
.=
const o,
(A . ii')
by A29, Th10
.=
(const o,(product Cs)) . i1
by A29, A42, Th10
;
:: thesis: verum end; hence
(const o,(product A)) | e = const o,
((product (A / EqR)) . e)
by A37, A38, A39, FUNCT_1:9;
:: thesis: verum end; now let x1 be
set ;
:: thesis: ( x1 in Class EqR implies g1 . x1 = (const o,(product (product (A / EqR)))) . x1 )assume
x1 in Class EqR
;
:: thesis: g1 . x1 = (const o,(product (product (A / EqR)))) . x1then reconsider e =
x1 as
Element of
Class EqR ;
consider f1 being
Function such that A43:
f1 = const o,
(product A)
;
g1 . e = f1 | e
by A22, A23, A31, A43;
hence g1 . x1 =
const o,
((product (A / EqR)) . e)
by A36, A43
.=
(const o,(product (product (A / EqR)))) . x1
by A29, Th10
;
:: thesis: verum end; then
(F . (the_result_sort_of o)) . (const o,(product A)) = const o,
(product (product (A / EqR)))
by A34, A35, FUNCT_1:9;
hence
(F . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(product (product (A / EqR)))) . (F # x)
by A29, A30, Th12;
:: thesis: verum end; suppose A44:
the_arity_of o <> {}
;
:: thesis: (F . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(product (product (A / EqR)))) . (F # x)A45:
(F . (the_result_sort_of o)) . ((Den o,(product A)) . x) in rng (F . (the_result_sort_of o))
by A25, A28, FUNCT_1:def 5;
then reconsider g1 =
(F . (the_result_sort_of o)) . ((Den o,(product A)) . x) as
Function by A24;
A46:
(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 ;
A47:
dom g1 =
dom (Carrier (product (A / EqR)),(the_result_sort_of o))
by A24, A45, CARD_3:18
.=
Class EqR
by PARTFUN1:def 4
;
A48:
dom f1 =
dom (Carrier (product (A / EqR)),(the_result_sort_of o))
by A46, CARD_3:18
.=
Class EqR
by PARTFUN1:def 4
;
A49:
now let e be
Element of
Class EqR;
:: thesis: 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 f2 be
Function;
:: thesis: ( f2 = (Den o,(product A)) . x implies f2 | e = (Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e) )assume A50:
f2 = (Den o,(product A)) . x
;
:: thesis: 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 A51:
(
Ji = (id (Class EqR)) . e &
Cs = (A / EqR) . e &
(product (A / EqR)) . e = product Cs )
by Def6;
dom f2 =
dom (Carrier A,(the_result_sort_of o))
by A28, A50, CARD_3:18
.=
I
by PARTFUN1:def 4
;
then A52:
dom (f2 | e) =
I /\ e
by RELAT_1:90
.=
e
by XBOOLE_1:28
;
A53:
(commute (F # x)) . e is
Element of
Args o,
((product (A / EqR)) . e)
by A44, Th21;
A54:
(commute (F # x)) . e is
Element of
Args o,
(product Cs)
by A44, A51, Th21;
A55:
(Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e) in product (Carrier Cs,(the_result_sort_of o))
by A51, A53, Th20;
then reconsider f3 =
(Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e) as
Function ;
A56:
dom f3 =
dom (Carrier Cs,(the_result_sort_of o))
by A55, CARD_3:18
.=
Ji
by PARTFUN1:def 4
.=
e
by A51, FUNCT_1:35
;
A57:
now let i1 be
Element of
I;
:: thesis: ( i1 in e implies (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 )assume A58:
i1 in e
;
:: thesis: (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1then reconsider i2 =
i1 as
Element of
Ji by A51, FUNCT_1:35;
(commute ((commute (F # x)) . e)) . i2 is
Element of
Args o,
(Cs . i2)
by A44, A51, A53, 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 A59:
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
;
(commute x) . i1 is
Element of
Args o,
(A . i1)
by A44, 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 A60:
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
;
now let n be
set ;
:: thesis: ( n in dom (the_arity_of o) implies ((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . n )assume A61:
n in dom (the_arity_of o)
;
:: thesis: ((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 ;
A62:
x . n in product (Carrier A,((the_arity_of o) /. n))
by A61, Th16;
then A63:
x . n in product (Carrier A,s1)
by A61, PARTFUN1:def 8;
reconsider f4 =
x . n as
Function by A62;
A64:
x . n in (SORTS A) . s1
by A63, PRALG_2:def 17;
dom f4 =
dom (Carrier A,s1)
by A63, CARD_3:18
.=
I
by PARTFUN1:def 4
;
then A65:
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 A61, 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 A66:
f7 = F . s1
and A67:
for
x' being
set st
x' in the
Sorts of
(product A) . s1 holds
S1[
f7 . x',
x',
s1]
by A20;
f5 =
(F . ((the_arity_of o) /. n)) . (x . n)
by A61, Th14
.=
f7 . (x . n)
by A61, A66, PARTFUN1:def 8
;
then A68:
f5 . e = f4 | e
by A64, A67;
then reconsider f6 =
f5 . e as
Function ;
f6 = ((commute (F # x)) . e) . n
by A61, Th22;
hence ((commute ((commute (F # x)) . e)) . i1) . n =
(f4 | e) . i2
by A51, A53, A61, A68, Th22
.=
f4 . i2
by A58, A65, FUNCT_1:70
.=
((commute x) . i1) . n
by A61, Th22
;
:: thesis: verum end; hence
(commute ((commute (F # x)) . e)) . i1 = (commute x) . i1
by A59, A60, FUNCT_1:9;
:: thesis: verum end; now let x1 be
set ;
:: thesis: ( x1 in e implies f3 . x1 = (f2 | e) . x1 )assume A69:
x1 in e
;
:: thesis: f3 . x1 = (f2 | e) . x1then reconsider i2 =
x1 as
Element of
Ji by A51, FUNCT_1:35;
reconsider i1 =
i2 as
Element of
I by A69;
A70:
dom (A | e) =
(dom A) /\ e
by RELAT_1:90
.=
I /\ e
by PARTFUN1:def 4
.=
e
by XBOOLE_1:28
;
Cs = A | e
by A51, Def5;
then
Cs . i2 = A . i1
by A69, A70, FUNCT_1:70;
hence f3 . x1 =
(Den o,(A . i1)) . ((commute ((commute (F # x)) . e)) . i2)
by A44, A51, A54, Th23
.=
(Den o,(A . i1)) . ((commute x) . i1)
by A57, A69
.=
f2 . x1
by A44, A50, Th23
.=
(f2 | e) . x1
by A52, A69, FUNCT_1:70
;
:: thesis: verum end; hence
f2 | e = (Den o,((product (A / EqR)) . e)) . ((commute (F # x)) . e)
by A52, A56, FUNCT_1:9;
:: thesis: verum end; hence
(F . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(product (product (A / EqR)))) . (F # x)
by A47, A48, FUNCT_1:9;
:: thesis: verum end;
end;
end;
A71:
F is "onto"
proof
let s be
set ;
:: according to MSUALG_3:def 3 :: thesis: ( not s in the carrier of S or proj2 (F . s) = the Sorts of (product (product (A / EqR))) . s )
assume A72:
s in the
carrier of
S
;
:: thesis: proj2 (F . s) = the Sorts of (product (product (A / EqR))) . s
reconsider s' =
s as
SortSymbol of
S by A72;
A73:
the
Sorts of
(product A) . s' = product (Carrier A,s')
by PRALG_2:def 17;
consider f being
Function of
(the Sorts of (product A) . s),
(the Sorts of (product (product (A / EqR))) . s) such that A75:
f = F . s
and A76:
for
x being
set st
x in the
Sorts of
(product A) . s holds
S1[
f . x,
x,
s]
by A20, A72;
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 ;
:: thesis: ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st
( x in dom f & y = f . x ) )
thus
(
y in the
Sorts of
(product (product (A / EqR))) . s iff ex
x being
set st
(
x in dom f &
y = f . x ) )
:: thesis: verumproof
thus
(
y in the
Sorts of
(product (product (A / EqR))) . s implies ex
x being
set st
(
x in dom f &
y = f . x ) )
:: thesis: ( ex x being set st
( x in dom f & y = f . x ) implies y in the Sorts of (product (product (A / EqR))) . s )proof
assume
y in the
Sorts of
(product (product (A / EqR))) . s
;
:: thesis: ex x being set st
( x in dom f & y = f . x )
then A77:
y in product (Carrier (product (A / EqR)),s')
by PRALG_2:def 17;
then consider gg being
Function such that A78:
(
y = gg &
dom gg = dom (Carrier (product (A / EqR)),s') )
and A79:
for
x' being
set st
x' in dom (Carrier (product (A / EqR)),s') holds
gg . x' in (Carrier (product (A / EqR)),s') . x'
by CARD_3:def 5;
reconsider y =
y as
Function by A77;
A80:
dom (Carrier (product (A / EqR)),s') = Class EqR
by PARTFUN1:def 4;
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 );
A81:
for
i being
set st
i in I holds
ex
j being
set st
S2[
i,
j]
proof
let i be
set ;
:: thesis: ( i in I implies ex j being set st S2[i,j] )
assume A82:
i in I
;
:: thesis: ex j being set st S2[i,j]
A83:
dom (Carrier (product (A / EqR)),s') = Class EqR
by PARTFUN1:def 4;
Class EqR,
i in Class EqR
by A82, EQREL_1:def 5;
then consider e being
Element of
Class EqR such that A84:
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 A85:
(product (A / EqR)) . e = product Cs
by Def6;
consider U0 being
MSAlgebra of
S such that A86:
(
U0 = (product (A / EqR)) . e &
(Carrier (product (A / EqR)),s') . e = the
Sorts of
U0 . s' )
by PRALG_2:def 16;
(Carrier (product (A / EqR)),s') . e = product (Carrier Cs,s')
by A85, A86, PRALG_2:def 17;
then reconsider y' =
y . e as
Function by A78, A79, A83, Lm1;
S2[
i,
y' . i]
by A82, A84, EQREL_1:28;
hence
ex
j being
set st
S2[
i,
j]
;
:: thesis: verum
end;
consider x being
ManySortedSet of
such that A87:
for
i being
set st
i in I holds
S2[
i,
x . i]
from PBOOLE:sch 3(A81);
A88:
x in the
Sorts of
(product A) . s'
proof
A89:
dom x =
I
by PARTFUN1:def 4
.=
dom (Carrier A,s')
by PARTFUN1:def 4
;
for
z being
set st
z in dom (Carrier A,s') holds
x . z in (Carrier A,s') . z
proof
let z be
set ;
:: thesis: ( z in dom (Carrier A,s') implies x . z in (Carrier A,s') . z )
assume
z in dom (Carrier A,s')
;
:: thesis: x . z in (Carrier A,s') . z
then
z in I
by PARTFUN1:def 4;
then consider e being
Element of
Class EqR,
f1 being
Function such that A90:
(
z in e &
f1 = y . e )
and A91:
x . z = f1 . z
by A87;
A92:
y . e in (Carrier (product (A / EqR)),s') . e
by A78, A79, A80;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A93:
Ji = (id (Class EqR)) . e
and A94:
Cs = (A / EqR) . e
and A95:
(product (A / EqR)) . e = product Cs
by Def6;
consider U0 being
MSAlgebra of
S such that A96:
(
U0 = (product (A / EqR)) . e &
(Carrier (product (A / EqR)),s') . e = the
Sorts of
U0 . s' )
by PRALG_2:def 16;
(Carrier (product (A / EqR)),s') . e = product (Carrier Cs,s')
by A95, A96, PRALG_2:def 17;
then consider g being
Function such that A97:
(
y . e = g &
dom g = dom (Carrier Cs,s') )
and A98:
for
x' being
set st
x' in dom (Carrier Cs,s') holds
g . x' in (Carrier Cs,s') . x'
by A92, CARD_3:def 5;
dom ((Carrier A,s') | e) =
(dom (Carrier A,s')) /\ e
by RELAT_1:90
.=
I /\ e
by PARTFUN1:def 4
.=
e
by XBOOLE_1:28
;
then A99:
((Carrier A,s') | e) . z = (Carrier A,s') . z
by A90, FUNCT_1:70;
A100:
Cs = A | e
by A94, Def5;
Ji = e
by A93, FUNCT_1:35;
then A101:
Carrier Cs,
s' = (Carrier A,s') | e
by A100, Th2;
dom (Carrier Cs,s') =
Ji
by PARTFUN1:def 4
.=
e
by A93, FUNCT_1:35
;
hence
x . z in (Carrier A,s') . z
by A90, A91, A97, A98, A99, A101;
:: thesis: verum
end;
hence
x in the
Sorts of
(product A) . s'
by A73, A89, CARD_3:18;
:: thesis: verum
end;
then A102:
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
f . x in product (Carrier (product (A / EqR)),s')
by PRALG_2:def 17;
then consider gg' being
Function such that A103:
(
f . x = gg' &
dom gg' = dom (Carrier (product (A / EqR)),s') )
and
for
x' being
set st
x' in dom (Carrier (product (A / EqR)),s') holds
gg' . x' in (Carrier (product (A / EqR)),s') . x'
by CARD_3:def 5;
reconsider f' =
f . x as
Function by A103;
y = f'
proof
for
e being
set st
e in Class EqR holds
y . e = f' . e
proof
let e be
set ;
:: thesis: ( e in Class EqR implies y . e = f' . e )
assume
e in Class EqR
;
:: thesis: y . e = f' . e
then reconsider e =
e as
Element of
Class EqR ;
A104:
y . e in (Carrier (product (A / EqR)),s') . e
by A78, A79, A80;
consider Ji being non
empty set ,
Cs being
MSAlgebra-Family of
Ji,
S such that A105:
Ji = (id (Class EqR)) . e
and
Cs = (A / EqR) . e
and A106:
(product (A / EqR)) . e = product Cs
by Def6;
consider U0 being
MSAlgebra of
S such that A107:
(
U0 = (product (A / EqR)) . e &
(Carrier (product (A / EqR)),s') . e = the
Sorts of
U0 . s' )
by PRALG_2:def 16;
(Carrier (product (A / EqR)),s') . e = product (Carrier Cs,s')
by A106, A107, PRALG_2:def 17;
then consider g being
Function such that A108:
(
y . e = g &
dom g = dom (Carrier Cs,s') )
and
for
x' being
set st
x' in dom (Carrier Cs,s') holds
g . x' in (Carrier Cs,s') . x'
by A104, CARD_3:def 5;
reconsider y' =
y . e as
Function by A108;
x | e = y'
hence
y . e = f' . e
by A76, A88;
:: thesis: verum
end;
hence
y = f'
by A78, A80, A103, FUNCT_1:9;
:: thesis: verum
end;
hence
ex
x being
set st
(
x in dom f &
y = f . x )
by A102;
:: thesis: verum
end;
thus
( ex
x being
set st
(
x in dom f &
y = f . x ) implies
y in the
Sorts of
(product (product (A / EqR))) . s )
:: thesis: verum
end;
end;
hence
proj2 (F . s) = the
Sorts of
(product (product (A / EqR))) . s
by A75, FUNCT_1:def 5;
:: thesis: verum
end;
A117:
F is "1-1"
proof
let s be
set ;
:: according to MSUALG_3:def 2 :: thesis: 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;
:: thesis: ( not s in proj1 F or not F . s = g or g is one-to-one )
assume A118:
(
s in dom F &
F . s = g )
;
:: thesis: g is one-to-one
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 g or not x2 in proj1 g or not g . x1 = g . x2 or x1 = x2 )
assume that A119:
x1 in dom g
and A120:
x2 in dom g
and A121:
g . x1 = g . x2
;
:: thesis: x1 = x2
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 A122:
f = F . s
and A123:
for
x being
set st
x in the
Sorts of
(product A) . s holds
S1[
f . x,
x,
s]
by A20, A118;
A124:
dom f = dom g
by A118, A122;
thus
x1 = x2
:: thesis: verumproof
reconsider s' =
s as
SortSymbol of
S by A118, PARTFUN1:def 4;
A125:
the
Sorts of
(product A) . s' = product (Carrier A,s')
by PRALG_2:def 17;
A126:
the
Sorts of
(product (product (A / EqR))) . s = product (Carrier (product (A / EqR)),s')
by PRALG_2:def 17;
consider gg being
Function such that A127:
x1 = gg
and A128:
dom gg = dom (Carrier A,s')
and
for
x' being
set st
x' in dom (Carrier A,s') holds
gg . x' in (Carrier A,s') . x'
by A119, A124, A125, CARD_3:def 5;
reconsider x1 =
x1 as
Function by A127;
consider gg1 being
Function such that A129:
x2 = gg1
and A130:
dom gg1 = dom (Carrier A,s')
and
for
x' being
set st
x' in dom (Carrier A,s') holds
gg1 . x' in (Carrier A,s') . x'
by A120, A124, A125, CARD_3:def 5;
reconsider x2 =
x2 as
Function by A129;
A131:
dom x1 = I
by A127, A128, PARTFUN1:def 4;
A132:
dom x2 = I
by A129, A130, PARTFUN1:def 4;
for
i being
set st
i in I holds
x1 . i = x2 . i
proof
let i be
set ;
:: thesis: ( i in I implies x1 . i = x2 . i )
assume A133:
i in I
;
:: thesis: x1 . i = x2 . i
then A134:
Class EqR,
i is
Element of
Class EqR
by EQREL_1:def 5;
reconsider f'' =
f . x2 as
Function by A120, A124, A126, Lm1, FUNCT_2:7;
x1 | (Class EqR,i) =
f'' . (Class EqR,i)
by A118, A119, A121, A122, A123, A124, A134
.=
x2 | (Class EqR,i)
by A120, A123, A124, A134
;
then x1 . i =
(x2 | (Class EqR,i)) . i
by A133, EQREL_1:28, FUNCT_1:72
.=
x2 . i
by A133, EQREL_1:28, FUNCT_1:72
;
hence
x1 . i = x2 . i
;
:: thesis: verum
end;
hence
x1 = x2
by A131, A132, FUNCT_1:9;
:: thesis: verum
end;
end;
F is_isomorphism product A, product (product (A / EqR))
hence
product A, product (product (A / EqR)) are_isomorphic
by MSUALG_3:def 13; :: thesis: verum