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