:: BIRKHOFF semantic presentation
:: deftheorem E1 defines -hash BIRKHOFF:def 1 :
theorem E2: :: BIRKHOFF:1
scheme :: BIRKHOFF:sch 1
s1{ F
1()
-> non
empty non
void ManySortedSign , F
2()
-> non-empty MSAlgebra of F
1(), P
1[
set ] } :
provided
proof
set c
1 = the
Sorts of F
2();
set c
2 = the
carrier of F
1();
set c
3 =
{ b1 where B is Element of (CongrLatt F2()) : ex b1 being MSCongruence of F2() st
( b2 = b1 & P1[ QuotMSAlg F2(),b2] ) } ;
defpred S
1[
set ] means ex b
1 being
MSCongruence of F
2() st
( b
1 = a
1 & P
1[
QuotMSAlg F
2(),b
1] );
E6:
{ b1 where B is Element of (CongrLatt F2()) : S1[b1] } is
Subset of
(CongrLatt F2())
from DOMAIN_1:sch 7();
consider c
4 being
empty set , c
5 being
MSAlgebra-Family of c
4,F
1();
for b
1 being
set holds
not ( b
1 in c
4 & ( for b
2 being
MSAlgebra of F
1() holds
not ( b
2 = c
5 . b
1 & P
1[b
2] ) ) )
;
then E8:
P
1[
product c
5]
by E5;
consider c
6 being
ManySortedSet of the
carrier of F
1()
such that E9:
{c6} = the
carrier of F
1()
--> {{} }
by MSUALG_9:6;
then
the
Sorts of
(product c5) = {c6}
by PBOOLE:3;
then
product c
5,
Trivial_Algebra F
1()
are_isomorphic
by MSUALG_9:27;
then E10:
P
1[
Trivial_Algebra F
1()]
by E3, E8;
[|the Sorts of F2(),the Sorts of F2()|] is
MSCongruence of F
2()
by MSUALG_5:20;
then E11:
[|the Sorts of F2(),the Sorts of F2()|] is
Element of
(CongrLatt F2())
by MSUALG_5:def 6;
reconsider c
7 =
[|the Sorts of F2(),the Sorts of F2()|] as
MSCongruence of F
2()
by MSUALG_5:20;
the
Sorts of
(QuotMSAlg F2(),c7) = {the Sorts of F2()}
by MSUALG_9:30;
then consider c
8 being
V2 ManySortedSet of the
carrier of F
1()
such that E12:
the
Sorts of
(QuotMSAlg F2(),c7) = {c8}
;
QuotMSAlg F
2(),c
7,
Trivial_Algebra F
1()
are_isomorphic
by E12, MSUALG_9:27;
then
Trivial_Algebra F
1(),
QuotMSAlg F
2(),c
7 are_isomorphic
by MSUALG_3:17;
then
P
1[
QuotMSAlg F
2(),c
7]
by E3, E10;
then E13:
[|the Sorts of F2(),the Sorts of F2()|] in { b1 where B is Element of (CongrLatt F2()) : ex b1 being MSCongruence of F2() st
( b2 = b1 & P1[ QuotMSAlg F2(),b2] ) }
by E11;
E14:
{ b1 where B is Element of (CongrLatt F2()) : ex b1 being MSCongruence of F2() st
( b2 = b1 & P1[ QuotMSAlg F2(),b2] ) } c= the
carrier of
(EqRelLatt the Sorts of F2())
then reconsider c
9 =
{ b1 where B is Element of (CongrLatt F2()) : ex b1 being MSCongruence of F2() st
( b2 = b1 & P1[ QuotMSAlg F2(),b2] ) } as non
empty SubsetFamily of
[|the Sorts of F2(),the Sorts of F2()|] by E13, MSUALG_7:6;
set c
10 =
meet |:c9:|;
E15:
meet |:c9:| is
MSEquivalence_Relation-like ManySortedRelation of the
Sorts of F
2()
by E14, MSUALG_7:9;
reconsider c
11 =
meet |:c9:| as
ManySortedRelation of F
2()
by E14, MSUALG_7:9;
c
11 is
MSEquivalence-like
then reconsider c
12 = c
11 as
MSEquivalence-like ManySortedRelation of F
2() ;
reconsider c
13 = c
12 as
MSCongruence of F
2()
by E6, MSUALG_9:29;
take c
14 =
QuotMSAlg F
2(),c
13;
defpred S
2[
set ,
set ] means ex b
1 being
MSCongruence of F
2() st
( b
1 = a
1 & a
2 = QuotMSAlg F
2(),b
1 );
E16:
now
let c
15 be
set ;
assume
c
15 in c
9
;
then reconsider c
16 = c
15 as
MSCongruence of F
2()
by E7;
consider c
17 being
set such that E17:
c
17 = QuotMSAlg F
2(),c
16
;
take c
18 = c
17;
thus
S
2[c
15,c
18]
by E17;
end;
consider c
15 being
ManySortedSet of c
9 such that E17:
for b
1 being
set holds
( b
1 in c
9 implies S
2[b
1,c
15 . b
1] )
from PBOOLE:sch 3(E16);
c
15 is
MSAlgebra-Family of c
9,F
1()
then reconsider c
16 = c
15 as
MSAlgebra-Family of c
9,F
1() ;
for b
1 being
set holds
not ( b
1 in c
9 & ( for b
2 being
MSAlgebra of F
1() holds
not ( b
2 = c
16 . b
1 & P
1[b
2] ) ) )
proof
let c
17 be
set ;
assume E18:
c
17 in c
9
;
then reconsider c
18 = c
17 as
Element of c
9 ;
take c
19 = c
16 . c
18;
consider c
20 being
Element of
(CongrLatt F2()) such that E19:
( c
17 = c
20 & ex b
1 being
MSCongruence of F
2() st
( b
1 = c
20 & P
1[
QuotMSAlg F
2(),b
1] ) )
by E18;
consider c
21 being
MSCongruence of F
2()
such that E20:
( c
21 = c
17 & c
16 . c
17 = QuotMSAlg F
2(),c
21 )
by E17, E18;
thus
( c
19 = c
16 . c
17 & P
1[c
19] )
by E19, E20;
end;
then E18:
P
1[
product c
16]
by E5;
reconsider c
17 =
MSNat_Hom F
2(),c
13 as
ManySortedFunction of F
2(),c
14 ;
take
c
17
;
defpred S
3[
Element of c
9,
set ] means ex b
1 being
ManySortedFunction of F
2(),
(c16 . a1) st
( b
1 = a
2 & b
1 is_homomorphism F
2(),c
16 . a
1 & ex b
2 being
MSCongruence of F
2() st
( a
1 = b
2 & b
1 = MSNat_Hom F
2(),b
2 ) );
E19:
for b
1 being
Element of c
9 holds
ex b
2 being
set st
S
3[b
1,b
2]
proof
let c
18 be
Element of c
9;
consider c
19 being
MSCongruence of F
2()
such that E20:
( c
19 = c
18 & c
16 . c
18 = QuotMSAlg F
2(),c
19 )
by E17;
set c
20 =
MSNat_Hom F
2(),c
19;
take
MSNat_Hom F
2(),c
19
;
reconsider c
21 =
MSNat_Hom F
2(),c
19 as
ManySortedFunction of F
2(),
(c16 . c18) by E20;
take
c
21
;
thus
c
21 = MSNat_Hom F
2(),c
19
;
MSNat_Hom F
2(),c
19 is_epimorphism F
2(),
QuotMSAlg F
2(),c
19
by MSUALG_4:3;
hence
c
21 is_homomorphism F
2(),c
16 . c
18
by E20, MSUALG_3:def 10;
take
c
19
;
thus
( c
18 = c
19 & c
21 = MSNat_Hom F
2(),c
19 )
by E20;
end;
consider c
18 being
ManySortedSet of c
9 such that E20:
for b
1 being
Element of c
9 holds
S
3[b
1,c
18 . b
1]
from MSUALG_9:sch 1(E19);
E21:
for b
1 being
Element of c
9 holds
ex b
2 being
ManySortedFunction of F
2(),
(c16 . b1) st
( b
2 = c
18 . b
1 & b
2 is_homomorphism F
2(),c
16 . b
1 )
c
18 is
Function-yielding
then reconsider c
19 = c
18 as
ManySortedFunction of c
9 ;
consider c
20 being
ManySortedFunction of F
2(),
(product c16) such that E22:
c
20 is_homomorphism F
2(),
product c
16
and E23:
for b
1 being
Element of c
9 holds
(proj c16,b1) ** c
20 = c
19 . b
1
by E21, PRALG_3:30;
MSHomQuot c
20 is_monomorphism QuotMSAlg F
2(),
(MSCng c20),
product c
16
by E22, MSUALG_4:4;
then E24:
QuotMSAlg F
2(),
(MSCng c20),
Image (MSHomQuot c20) are_isomorphic
by MSUALG_9:17;
now
let c
21 be
set ;
assume
c
21 in the
carrier of F
1()
;
then reconsider c
22 = c
21 as
SortSymbol of F
1() ;
consider c
23 being
Subset-Family of
([|the Sorts of F2(),the Sorts of F2()|] . c22) such that E25:
c
23 = |:c9:| . c
22
and E26:
(meet |:c9:|) . c
22 = Intersect c
23
by MSSUBFAM:def 2;
E27:
|:c9:| . c
22 = { (b1 . c22) where B is Element of Bool [|the Sorts of F2(),the Sorts of F2()|] : b1 in c9 }
by CLOSURE2:15;
(MSCng c20) . c
22 = c
13 . c
22
proof
let c
24, c
25 be
set ;
:: according to RELAT_1:def 2
hereby
assume E28:
[c24,c25] in (MSCng c20) . c
22
;
then E29:
( c
24 in the
Sorts of F
2()
. c
22 & c
25 in the
Sorts of F
2()
. c
22 )
by ZFMISC_1:106;
[c24,c25] in [:(the Sorts of F2() . c22),(the Sorts of F2() . c22):]
by E28;
then E30:
[c24,c25] in [|the Sorts of F2(),the Sorts of F2()|] . c
22
by PBOOLE:def 21;
E31:
[c24,c25] in MSCng c
20,c
22
by E22, E28, MSUALG_4:def 20;
for b
1 being
set holds
( b
1 in c
23 implies
[c24,c25] in b
1 )
proof
let c
26 be
set ;
assume
c
26 in c
23
;
then consider c
27 being
Element of
Bool [|the Sorts of F2(),the Sorts of F2()|] such that E32:
c
26 = c
27 . c
22
and E33:
c
27 in c
9
by E25, E27;
reconsider c
28 = c
27 as
Element of c
9 by E33;
consider c
29 being
ManySortedFunction of F
2(),
(c16 . c28) such that E34:
( c
29 = c
19 . c
28 & c
29 is_homomorphism F
2(),c
16 . c
28 & ex b
1 being
MSCongruence of F
2() st
( c
28 = b
1 & c
29 = MSNat_Hom F
2(),b
1 ) )
by E20;
consider c
30 being
MSCongruence of F
2()
such that E35:
( c
28 = c
30 & c
29 = MSNat_Hom F
2(),c
30 )
by E34;
(c29 . c22) . c
24 =
(((proj c16,c28) ** c20) . c22) . c
24
by E23, E34
.=
(((proj c16,c28) . c22) * (c20 . c22)) . c
24
by MSUALG_3:2
.=
((proj c16,c28) . c22) . ((c20 . c22) . c24)
by E29, FUNCT_2:21
.=
((proj c16,c28) . c22) . ((c20 . c22) . c25)
by E29, E31, MSUALG_4:def 19
.=
(((proj c16,c28) . c22) * (c20 . c22)) . c
25
by E29, FUNCT_2:21
.=
(((proj c16,c28) ** c20) . c22) . c
25
by MSUALG_3:2
.=
(c29 . c22) . c
25
by E23, E34
;
hence
[c24,c25] in c
26
by E29, E32, E35, MSUALG_9:34;
end;
hence
[c24,c25] in c
13 . c
22
by E26, E30, SETFAM_1:58;
end;
assume E28:
[c24,c25] in c
13 . c
22
;
then E29:
( c
24 in the
Sorts of F
2()
. c
22 & c
25 in the
Sorts of F
2()
. c
22 )
by ZFMISC_1:106;
(c20 . c22) . c
24 in the
Sorts of
(product c16) . c
22
by E29, FUNCT_2:7;
then E30:
(c20 . c22) . c
24 in product (Carrier c16,c22)
by PRALG_2:def 17;
(c20 . c22) . c
25 in the
Sorts of
(product c16) . c
22
by E29, FUNCT_2:7;
then E31:
(c20 . c22) . c
25 in product (Carrier c16,c22)
by PRALG_2:def 17;
for b
1 being
Element of c
9 holds
(proj (Carrier c16,c22),b1) . ((c20 . c22) . c24) = (proj (Carrier c16,c22),b1) . ((c20 . c22) . c25)
proof
let c
26 be
Element of c
9;
reconsider c
27 = c
26 as
MSCongruence of F
2()
by E7;
c
27 is
Element of
Bool [|the Sorts of F2(),the Sorts of F2()|]
by CLOSURE2:def 1;
then
c
27 . c
22 in |:c9:| . c
22
by E27;
then E32:
[c24,c25] in c
27 . c
22
by E25, E26, E28, SETFAM_1:58;
consider c
28 being
ManySortedFunction of F
2(),
(c16 . c26) such that E33:
( c
28 = c
19 . c
26 & c
28 is_homomorphism F
2(),c
16 . c
26 & ex b
1 being
MSCongruence of F
2() st
( c
26 = b
1 & c
28 = MSNat_Hom F
2(),b
1 ) )
by E20;
consider c
29 being
MSCongruence of F
2()
such that E34:
( c
27 = c
29 & c
28 = MSNat_Hom F
2(),c
29 )
by E33;
thus (proj (Carrier c16,c22),c26) . ((c20 . c22) . c24) =
((proj c16,c26) . c22) . ((c20 . c22) . c24)
by PRALG_3:def 3
.=
(((proj c16,c26) . c22) * (c20 . c22)) . c
24
by E29, FUNCT_2:21
.=
(((proj c16,c26) ** c20) . c22) . c
24
by MSUALG_3:2
.=
(c28 . c22) . c
24
by E23, E33
.=
(c28 . c22) . c
25
by E29, E32, E34, MSUALG_9:34
.=
(((proj c16,c26) ** c20) . c22) . c
25
by E23, E33
.=
(((proj c16,c26) . c22) * (c20 . c22)) . c
25
by MSUALG_3:2
.=
((proj c16,c26) . c22) . ((c20 . c22) . c25)
by E29, FUNCT_2:21
.=
(proj (Carrier c16,c22),c26) . ((c20 . c22) . c25)
by PRALG_3:def 3
;
end;
then
(c20 . c22) . c
24 = (c20 . c22) . c
25
by E30, E31, MSUALG_9:15;
then
[c24,c25] in MSCng c
20,c
22
by E29, MSUALG_4:def 19;
hence
[c24,c25] in (MSCng c20) . c
22
by E22, MSUALG_4:def 20;
end;
hence
(MSCng c20) . c
21 = c
13 . c
21
;
end;
then
MSCng c
20 = c
13
by PBOOLE:3;
then consider c
21 being
strict non-empty MSSubAlgebra of
product c
16 such that E25:
c
14,c
21 are_isomorphic
by E24;
E26:
c
21,c
14 are_isomorphic
by E25, MSUALG_3:17;
P
1[c
21]
by E4, E18;
hence
P
1[c
14]
by E3, E26;
thus E27:
c
17 is_epimorphism F
2(),c
14
by MSUALG_4:3;
let c
22 be
non-empty MSAlgebra of F
1();
let c
23 be
ManySortedFunction of F
2(),c
22;
assume that E28:
c
23 is_homomorphism F
2(),c
22
and E29:
P
1[c
22]
;
reconsider c
24 =
Image (MSHomQuot c23) as
strict non-empty MSSubAlgebra of c
22 ;
MSHomQuot c
23 is_monomorphism QuotMSAlg F
2(),
(MSCng c23),c
22
by E28, MSUALG_4:4;
then
QuotMSAlg F
2(),
(MSCng c23),c
24 are_isomorphic
by MSUALG_9:17;
then E30:
c
24,
QuotMSAlg F
2(),
(MSCng c23) are_isomorphic
by MSUALG_3:17;
E31:
MSCng c
23 is
Element of
(CongrLatt F2())
by MSUALG_5:def 6;
P
1[c
24]
by E4, E29;
then
P
1[
QuotMSAlg F
2(),
(MSCng c23)]
by E3, E30;
then
MSCng c
23 in c
9
by E31;
then
MSCng c
23 in |:c9:|
by CLOSURE2:22;
then
c
13 c= MSCng c
23
by MSSUBFAM:43;
then consider c
25 being
ManySortedFunction of c
14,c
22 such that E32:
( c
25 is_homomorphism c
14,c
22 & c
23 = c
25 ** c
17 )
by E28, MSUALG_9:37;
take
c
25
;
thus
c
25 is_homomorphism c
14,c
22
by E32;
thus
c
23 = c
25 ** c
17
by E32;
let c
26 be
ManySortedFunction of c
14,c
22;
assume E33:
c
26 ** c
17 = c
23
;
c
17 is
"onto"
by E27, MSUALG_3:def 10;
hence
c
25 = c
26
by E32, E33, EXTENS_1:16;
end;
scheme :: BIRKHOFF:sch 2
s2{ F
1()
-> non
empty non
void ManySortedSign , F
2()
-> V2 ManySortedSet of the
carrier of F
1(), P
1[
set ] } :
provided
proof
set c
1 =
FreeMSA F
2();
E6:
for b
1, b
2 being
non-empty MSAlgebra of F
1() holds
( ( b
1,b
2 are_isomorphic & P
1[b
1] ) implies ( P
1[b
2] ) )
by E3;
E7:
for b
1 being
non-empty MSAlgebra of F
1()
for b
2 being
strict non-empty MSSubAlgebra of b
1 holds
( P
1[b
1] implies P
1[b
2] )
by E4;
E8:
for b
1 being
set for b
2 being
MSAlgebra-Family of b
1,F
1() holds
( ( for b
3 being
set holds
not ( b
3 in b
1 & ( for b
4 being
MSAlgebra of F
1() holds
not ( b
4 = b
2 . b
3 & P
1[b
4] ) ) ) ) implies P
1[
product b
2] )
by E5;
consider c
2 being
strict non-empty MSAlgebra of F
1(), c
3 being
ManySortedFunction of
(FreeMSA F2()),c
2 such that E9:
P
1[c
2]
and E10:
c
3 is_epimorphism FreeMSA F
2(),c
2
and E11:
for b
1 being
non-empty MSAlgebra of F
1()
for b
2 being
ManySortedFunction of
(FreeMSA F2()),b
1 holds
not ( b
2 is_homomorphism FreeMSA F
2(),b
1 & P
1[b
1] & ( for b
3 being
ManySortedFunction of c
2,b
1 holds
not ( b
3 is_homomorphism c
2,b
1 & b
3 ** c
3 = b
2 & ( for b
4 being
ManySortedFunction of c
2,b
1 holds
( b
4 ** c
3 = b
2 implies b
3 = b
4 ) ) ) ) )
from BIRKHOFF:sch 1(E6, E7, E8);
take
c
2
;
reconsider c
4 =
(c3 || (FreeGen F2())) ** ((Reverse F2()) "" ) as
ManySortedFunction of F
2(),the
Sorts of c
2 ;
take
c
4
;
thus
P
1[c
2]
by E9;
let c
5 be
non-empty MSAlgebra of F
1();
let c
6 be
ManySortedFunction of F
2(),the
Sorts of c
5;
assume E12:
P
1[c
5]
;
consider c
7 being
ManySortedFunction of
(FreeMSA F2()),c
5 such that E13:
c
7 is_homomorphism FreeMSA F
2(),c
5
and E14:
c
7 || (FreeGen F2()) = c
6 ** (Reverse F2())
by MSAFREE:def 5;
consider c
8 being
ManySortedFunction of c
2,c
5 such that E15:
c
8 is_homomorphism c
2,c
5
and E16:
c
8 ** c
3 = c
7
and
for b
1 being
ManySortedFunction of c
2,c
5 holds
( b
1 ** c
3 = c
7 implies c
8 = b
1 )
by E11, E12, E13;
take
c
8
;
thus
c
8 is_homomorphism c
2,c
5
by E15;
rngs (Reverse F2()) = F
2()
by EXTENS_1:14;
then E17:
Reverse F
2() is
"onto"
by EXTENS_1:13;
E18:
Reverse F
2() is
"1-1"
by MSUALG_9:12;
E19: c
4 ** (Reverse F2()) =
(c3 || (FreeGen F2())) ** (((Reverse F2()) "" ) ** (Reverse F2()))
by AUTALG_1:13
.=
(c3 || (FreeGen F2())) ** (id (FreeGen F2()))
by E17, E18, MSUALG_3:5
.=
c
3 || (FreeGen F2())
by MSUALG_3:3
;
c
8 ** (c3 || (FreeGen F2())) = c
7 || (FreeGen F2())
by E16, EXTENS_1:8;
then E20:
(c8 ** c4) ** (Reverse F2()) = c
6 ** (Reverse F2())
by E14, E19, AUTALG_1:13;
hence
c
8 ** c
4 = c
6
by E17, EXTENS_1:16;
E21:
c
3 is
"onto"
by E10, MSUALG_3:def 10;
E22:
c
3 is_homomorphism FreeMSA F
2(),c
2
by E10, MSUALG_3:def 10;
let c
9 be
ManySortedFunction of c
2,c
5;
assume
c
9 is_homomorphism c
2,c
5
;
then E23:
c
9 ** c
3 is_homomorphism FreeMSA F
2(),c
5
by E22, MSUALG_3:10;
assume
c
9 ** c
4 = c
6
;
then
c
9 ** (((c3 || (FreeGen F2())) ** ((Reverse F2()) "" )) ** (Reverse F2())) = (c8 ** ((c3 || (FreeGen F2())) ** ((Reverse F2()) "" ))) ** (Reverse F2())
by E20, AUTALG_1:13;
then
c
9 ** (((c3 || (FreeGen F2())) ** ((Reverse F2()) "" )) ** (Reverse F2())) = c
8 ** (((c3 || (FreeGen F2())) ** ((Reverse F2()) "" )) ** (Reverse F2()))
by AUTALG_1:13;
then
c
9 ** ((c3 || (FreeGen F2())) ** (((Reverse F2()) "" ) ** (Reverse F2()))) = c
8 ** (((c3 || (FreeGen F2())) ** ((Reverse F2()) "" )) ** (Reverse F2()))
by AUTALG_1:13;
then
c
9 ** ((c3 || (FreeGen F2())) ** (((Reverse F2()) "" ) ** (Reverse F2()))) = c
8 ** ((c3 || (FreeGen F2())) ** (((Reverse F2()) "" ) ** (Reverse F2())))
by AUTALG_1:13;
then
c
9 ** ((c3 || (FreeGen F2())) ** (id (FreeGen F2()))) = c
8 ** ((c3 || (FreeGen F2())) ** (((Reverse F2()) "" ) ** (Reverse F2())))
by E17, E18, MSUALG_3:5;
then
c
9 ** ((c3 || (FreeGen F2())) ** (id (FreeGen F2()))) = c
8 ** ((c3 || (FreeGen F2())) ** (id (FreeGen F2())))
by E17, E18, MSUALG_3:5;
then
c
9 ** (c3 || (FreeGen F2())) = c
8 ** ((c3 || (FreeGen F2())) ** (id (FreeGen F2())))
by MSUALG_3:3;
then
c
9 ** (c3 || (FreeGen F2())) = c
8 ** (c3 || (FreeGen F2()))
by MSUALG_3:3;
then
(c9 ** c3) || (FreeGen F2()) = c
8 ** (c3 || (FreeGen F2()))
by EXTENS_1:8;
then
(c9 ** c3) || (FreeGen F2()) = (c8 ** c3) || (FreeGen F2())
by EXTENS_1:8;
then
c
9 ** c
3 = c
8 ** c
3
by E13, E16, E23, EXTENS_1:18;
hence
c
8 = c
9
by E21, EXTENS_1:16;
end;
scheme :: BIRKHOFF:sch 3
s3{ F
1()
-> non
empty non
void ManySortedSign , F
2()
-> non-empty MSAlgebra of F
1(), F
3()
-> non-empty MSAlgebra of F
1(), F
4()
-> ManySortedFunction of the
carrier of F
1()
--> NAT ,the
Sorts of F
2(), F
5()
-> ManySortedFunction of the
carrier of F
1()
--> NAT ,the
Sorts of F
3(), P
1[
set ] } :
provided
proof
reconsider c
1 = the
carrier of F
1()
--> NAT as
V2 ManySortedSet of the
carrier of F
1() ;
consider c
2 being
ManySortedFunction of F
2(),F
3()
such that E5:
c
2 is_homomorphism F
2(),F
3()
and E6:
F
5()
= c
2 ** F
4()
by E3, E4;
reconsider c
3 = F
5() as
ManySortedFunction of c
1,the
Sorts of F
3() ;
E7:
c
3 -hash is_homomorphism FreeMSA c
1,F
3()
by E1;
F
4()
-hash is_homomorphism FreeMSA (the carrier of F1() --> NAT ),F
2()
by E1;
then E8:
c
2 ** (F4() -hash ) is_homomorphism FreeMSA (the carrier of F1() --> NAT ),F
3()
by E5, MSUALG_3:10;
E9:
(c3 -hash ) || (FreeGen c1) =
F
5()
** (Reverse c1)
by E1
.=
c
2 ** (F4() ** (Reverse c1))
by E6, AUTALG_1:13
.=
c
2 ** ((F4() -hash ) || (FreeGen (the carrier of F1() --> NAT )))
by E1
.=
(c2 ** (F4() -hash )) || (FreeGen (the carrier of F1() --> NAT ))
by EXTENS_1:8
;
take
c
2
;
thus
c
2 is_homomorphism F
2(),F
3()
by E5;
thus
F
5()
-hash = c
2 ** (F4() -hash )
by E7, E8, E9, EXTENS_1:18;
end;
scheme :: BIRKHOFF:sch 4
s4{ F
1()
-> non
empty non
void ManySortedSign , F
2()
-> non-empty MSAlgebra of F
1(), F
3()
-> ManySortedFunction of the
carrier of F
1()
--> NAT ,the
Sorts of F
2(), F
4()
-> SortSymbol of F
1(), F
5()
-> Element of the
Sorts of
(TermAlg F1()) . F
4(), F
6()
-> Element of the
Sorts of
(TermAlg F1()) . F
4(), P
1[
set ] } :
provided
proof
reconsider c
1 = the
carrier of F
1()
--> NAT as
V2 ManySortedSet of the
carrier of F
1() ;
let c
2 be
non-empty MSAlgebra of F
1();
assume E5:
P
1[c
2]
;
let c
3 be
ManySortedFunction of
(TermAlg F1()),c
2;
:: according to EQUATION:def 5
assume E6:
c
3 is_homomorphism TermAlg F
1(),c
2
;
reconsider c
4 = c
3 as
ManySortedFunction of
(FreeMSA c1),c
2 ;
set c
5 =
(c4 || (FreeGen c1)) ** ((Reverse c1) "" );
reconsider c
6 =
(c4 || (FreeGen c1)) ** ((Reverse c1) "" ) as
ManySortedFunction of the
carrier of F
1()
--> NAT ,the
Sorts of c
2 ;
reconsider c
7 = F
3() as
ManySortedFunction of the
carrier of F
1()
--> NAT ,the
Sorts of F
2() ;
E7:
P
1[c
2]
by E5;
E8:
for b
1 being
non-empty MSAlgebra of F
1()
for b
2 being
ManySortedFunction of the
carrier of F
1()
--> NAT ,the
Sorts of b
1 holds
not ( P
1[b
1] & ( for b
3 being
ManySortedFunction of F
2(),b
1 holds
not ( b
3 is_homomorphism F
2(),b
1 & b
2 = b
3 ** c
7 ) ) )
by E4;
consider c
8 being
ManySortedFunction of F
2(),c
2 such that
c
8 is_homomorphism F
2(),c
2
and E9:
c
6 -hash = c
8 ** (c7 -hash )
from BIRKHOFF:sch 3(E7, E8);
E10:
((c4 || (FreeGen c1)) ** ((Reverse c1) "" )) -hash is_homomorphism FreeMSA c
1,c
2
by E1;
rngs (Reverse c1) = c
1
by EXTENS_1:14;
then E11:
(
Reverse c
1 is
"1-1" &
Reverse c
1 is
"onto" )
by EXTENS_1:13, MSUALG_9:12;
(((c4 || (FreeGen c1)) ** ((Reverse c1) "" )) -hash ) || (FreeGen c1) =
((c4 || (FreeGen c1)) ** ((Reverse c1) "" )) ** (Reverse c1)
by E1
.=
(c4 || (FreeGen c1)) ** (((Reverse c1) "" ) ** (Reverse c1))
by AUTALG_1:13
.=
(c4 || (FreeGen c1)) ** (id (FreeGen c1))
by E11, MSUALG_3:5
.=
c
4 || (FreeGen c1)
by MSUALG_3:3
;
then E12:
((c4 || (FreeGen c1)) ** ((Reverse c1) "" )) -hash = c
4
by E6, E10, EXTENS_1:18;
E13:
((((c4 || (FreeGen c1)) ** ((Reverse c1) "" )) -hash ) . F4()) . F
5() =
((c8 . F4()) * ((F3() -hash ) . F