{} in {{}} *
by FINSEQ_1:66;
then reconsider f = {[{},{{}}]} --> {} as Function of {[{},{{}}]},({{}} *) by FUNCOP_1:58;
reconsider g = {[{},{{}}]} --> {} as Function of {[{},{{}}]},{{}} ;
take S = ManySortedSign(# {{}},{[{},{{}}]},f,g #); ( not S is void & S is finite & S is monotonic & S is Circuit-like )
thus
not S is void
; ( S is finite & S is monotonic & S is Circuit-like )
thus
S is finite
; ( S is monotonic & S is Circuit-like )
thus
S is monotonic
S is Circuit-like proof
reconsider S9 =
S as non
empty non
void ManySortedSign ;
let A be
non-empty finitely-generated MSAlgebra of
S;
MSAFREE2:def 13 A is finite-yielding
reconsider A9 =
A as
non-empty MSAlgebra of
S9 ;
consider s being
SortSymbol of
S9;
consider G being
GeneratorSet of
A9 such that A1:
G is
finite-yielding
by Def10;
reconsider Gs =
G . s as
finite set by A1, FINSET_1:def 4;
consider o being
OperSymbol of
S9;
set T =
s .--> ((G . s) \/ {((Den (o,A9)) . {})});
set O =
o .--> (Den (o,A9));
reconsider G9 =
G as
MSSubset of
A9 ;
let i be
set ;
FINSET_1:def 4,
MSAFREE2:def 11 ( not i in the carrier of S or the Sorts of A . i is finite )
A2:
s = {}
by TARSKI:def 1;
then reconsider T =
s .--> ((G . s) \/ {((Den (o,A9)) . {})}) as
V16()
ManySortedSet of the
carrier of
S ;
assume
i in the
carrier of
S
;
the Sorts of A . i is finite
then A3:
i = s
by A2, TARSKI:def 1;
reconsider T9 =
T as
ManySortedSet of the
carrier of
S9 ;
A4:
Args (
o,
A9) =
( the Sorts of A9 #) . ( the Arity of S . o)
by FUNCT_2:21
.=
( the Sorts of A9 #) . (<*> the carrier of S9)
by FUNCOP_1:13
.=
{{}}
by PRE_CIRC:5
;
then A5:
dom (Den (o,A9)) = {{}}
by FUNCT_2:def 1;
A6:
now let i be
set ;
( i in the carrier' of S implies (o .--> (Den (o,A9))) . i is Function of (((T #) * the Arity of S) . i),((T * the ResultSort of S) . i) )assume A7:
i in the
carrier' of
S
;
(o .--> (Den (o,A9))) . i is Function of (((T #) * the Arity of S) . i),((T * the ResultSort of S) . i)then
i = [{},{{}}]
by TARSKI:def 1;
then A8:
i = o
by TARSKI:def 1;
((T #) * the Arity of S) . i =
(T #) . ( the Arity of S . i)
by A7, FUNCT_2:21
.=
(T #) . (<*> the carrier of S)
by A7, FUNCOP_1:13
.=
{{}}
by PRE_CIRC:5
;
then reconsider Oi =
(o .--> (Den (o,A9))) . i as
Function of
(((T #) * the Arity of S) . i),
(Result (o,A9)) by A4, A8, FUNCOP_1:87;
(o .--> (Den (o,A9))) . i = Den (
o,
A9)
by A8, FUNCOP_1:87;
then A9:
rng Oi = {((Den (o,A9)) . {})}
by A5, FUNCT_1:14;
(T * the ResultSort of S) . i =
T . ( the ResultSort of S . i)
by A7, FUNCT_2:21
.=
T . s
by A2, A7, FUNCOP_1:13
.=
(G . s) \/ {((Den (o,A9)) . {})}
by FUNCOP_1:87
;
then
rng Oi c= (T * the ResultSort of S) . i
by A9, XBOOLE_1:7;
hence
(o .--> (Den (o,A9))) . i is
Function of
(((T #) * the Arity of S) . i),
((T * the ResultSort of S) . i)
by FUNCT_2:8;
verum end;
A10:
o = [{},{{}}]
by TARSKI:def 1;
then reconsider O =
o .--> (Den (o,A9)) as
ManySortedFunction of
(T #) * the
Arity of
S,
T * the
ResultSort of
S by A6, PBOOLE:def 18;
A11:
now let B be
MSSubset of
A9;
( B = the Sorts of MSAlgebra(# T,O #) implies ( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers (A9,B) ) )assume A12:
B = the
Sorts of
MSAlgebra(#
T,
O #)
;
( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers (A9,B) )thus A13:
B is
opers_closed
the Charact of MSAlgebra(# T,O #) = Opers (A9,B)proof
let o9 be
OperSymbol of
S9;
MSUALG_2:def 7 B is_closed_on o9let x be
set ;
TARSKI:def 3,
MSUALG_2:def 6 ( not x in proj2 ((Den (o9,A9)) | (( the Arity of S9 * (B #)) . o9)) or x in ( the ResultSort of S9 * B) . o9 )
assume A14:
x in rng ((Den (o9,A9)) | (((B #) * the Arity of S9) . o9))
;
x in ( the ResultSort of S9 * B) . o9
A15:
o9 = o
by A10, TARSKI:def 1;
A16:
(
dom the
ResultSort of
S9 = {[{},{{}}]} & the
ResultSort of
S9 . o = s )
by A2, FUNCOP_1:13, FUNCOP_1:19;
A17:
(Den (o,A9)) | {{}} = Den (
o,
A9)
by A5, RELAT_1:97;
((B #) * the Arity of S) . o =
(B #) . ( the Arity of S . o)
by FUNCT_2:21
.=
(T #) . (<*> the carrier of S)
by A12, FUNCOP_1:13
.=
{{}}
by PRE_CIRC:5
;
then
ex
y being
set st
(
y in dom (Den (o,A9)) &
x = (Den (o,A9)) . y )
by A15, A17, A14, FUNCT_1:def 5;
then
x = (Den (o,A9)) . {}
by A4, TARSKI:def 1;
then A18:
x in {((Den (o,A9)) . {})}
by TARSKI:def 1;
B . s = (G . s) \/ {((Den (o,A9)) . {})}
by A12, FUNCOP_1:87;
then
x in B . s
by A18, XBOOLE_0:def 3;
hence
x in ( the ResultSort of S9 * B) . o9
by A15, A16, FUNCT_1:23;
verum
end; now let o9 be
OperSymbol of
S9;
the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B((B #) * the Arity of S9) . o =
(B #) . ( the Arity of S9 . o)
by FUNCT_2:21
.=
(T #) . (<*> the carrier of S9)
by A12, FUNCOP_1:13
.=
{{}}
by PRE_CIRC:5
;
then
(Den (o,A9)) | (((B #) * the Arity of S9) . o) = Den (
o,
A9)
by A5, RELAT_1:97;
then A19:
the
Charact of
MSAlgebra(#
T,
O #)
. o = (Den (o,A9)) | (((B #) * the Arity of S9) . o)
by FUNCOP_1:87;
(
o9 = o &
B is_closed_on o )
by A10, A13, MSUALG_2:def 7, TARSKI:def 1;
hence
the
Charact of
MSAlgebra(#
T,
O #)
. o9 = o9 /. B
by A19, MSUALG_2:def 8;
verum end; hence
the
Charact of
MSAlgebra(#
T,
O #)
= Opers (
A9,
B)
by A12, MSUALG_2:def 9;
verum end;
reconsider A99 =
MSAlgebra(#
T,
O #) as
non-empty MSAlgebra of
S9 by MSUALG_1:def 8;
A20:
Result (
o,
A9) =
the
Sorts of
A9 . ( the ResultSort of S . o)
by FUNCT_2:21
.=
the
Sorts of
A9 . {}
by FUNCOP_1:13
;
T9 c= the
Sorts of
A9
proof
let i be
set ;
PBOOLE:def 5 ( not i in the carrier of S9 or T9 . i c= the Sorts of A9 . i )
assume
i in the
carrier of
S9
;
T9 . i c= the Sorts of A9 . i
then A21:
i = {}
by TARSKI:def 1;
then A22:
T9 . i = (G . s) \/ {((Den (o,A9)) . {})}
by A2, FUNCOP_1:87;
G c= the
Sorts of
A9
by PBOOLE:def 23;
then A23:
G . s c= the
Sorts of
A9 . i
by A2, A21, PBOOLE:def 5;
dom (Den (o,A9)) = Args (
o,
A9)
by FUNCT_2:def 1;
then
{} in dom (Den (o,A9))
by A4, TARSKI:def 1;
then
(Den (o,A9)) . {} in rng (Den (o,A9))
by FUNCT_1:def 5;
then
{((Den (o,A9)) . {})} c= the
Sorts of
A9 . i
by A20, A21, ZFMISC_1:37;
hence
T9 . i c= the
Sorts of
A9 . i
by A22, A23, XBOOLE_1:8;
verum
end;
then
the
Sorts of
MSAlgebra(#
T,
O #) is
MSSubset of
A9
by PBOOLE:def 23;
then reconsider A99 =
A99 as
strict MSSubAlgebra of
A9 by A11, MSUALG_2:def 10;
A24:
now let U1 be
MSSubAlgebra of
A9;
( G9 is MSSubset of U1 implies A99 is MSSubAlgebra of U1 )assume A25:
G9 is
MSSubset of
U1
;
A99 is MSSubAlgebra of U1now
Constants A9 is
MSSubset of
U1
by MSUALG_2:11;
then
Constants A9 c= the
Sorts of
U1
by PBOOLE:def 23;
then
(Constants A9) . s c= the
Sorts of
U1 . s
by PBOOLE:def 5;
then A26:
Constants (
A9,
s)
c= the
Sorts of
U1 . s
by MSUALG_2:def 5;
A27:
{} in dom (Den (o,A9))
by A5, TARSKI:def 1;
then
(Den (o,A9)) . {} in rng (Den (o,A9))
by FUNCT_1:def 5;
then reconsider b =
(Den (o,A9)) . {} as
Element of the
Sorts of
A9 . s by A20, TARSKI:def 1;
let i be
set ;
( i in the carrier of S9 implies the Sorts of A99 . i c= the Sorts of U1 . i )A28:
( the
Arity of
S9 . o = {} & ex
X being non
empty set st
(
X = the
Sorts of
A9 . s &
Constants (
A9,
s)
= { a where a is Element of X : ex o being OperSymbol of S9 st
( the Arity of S9 . o = {} & the ResultSort of S9 . o = s & a in rng (Den (o,A9)) ) } ) )
by FUNCOP_1:13, MSUALG_2:def 4;
b in rng (Den (o,A9))
by A27, FUNCT_1:def 5;
then
(Den (o,A9)) . {} in Constants (
A9,
s)
by A2, A28;
then A29:
{((Den (o,A9)) . {})} c= the
Sorts of
U1 . s
by A26, ZFMISC_1:37;
G c= the
Sorts of
U1
by A25, PBOOLE:def 23;
then A30:
( the
Sorts of
A99 . s = (G . s) \/ {((Den (o,A9)) . {})} &
G . s c= the
Sorts of
U1 . s )
by FUNCOP_1:87, PBOOLE:def 5;
assume
i in the
carrier of
S9
;
the Sorts of A99 . i c= the Sorts of U1 . ithen
i = s
by A2, TARSKI:def 1;
hence
the
Sorts of
A99 . i c= the
Sorts of
U1 . i
by A30, A29, XBOOLE_1:8;
verum end; then
the
Sorts of
A99 c= the
Sorts of
U1
by PBOOLE:def 5;
hence
A99 is
MSSubAlgebra of
U1
by MSUALG_2:9;
verum end;
then
G9 c= the
Sorts of
A99
by PBOOLE:def 5;
then
G9 is
MSSubset of
A99
by PBOOLE:def 23;
then s .--> ((G . s) \/ {((Den (o,A9)) . {})}) =
the
Sorts of
(GenMSAlg G)
by A24, MSUALG_2:def 18
.=
the
Sorts of
A9
by MSAFREE:def 4
;
then
the
Sorts of
A . i = Gs \/ {((Den (o,A9)) . {})}
by A3, FUNCOP_1:87;
hence
the
Sorts of
A . i is
finite
;
verum
end;
thus
S is Circuit-like
verum