{} 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 #); :: thesis: ( not S is void & S is finite & S is monotonic & S is Circuit-like )
thus not S is void ; :: thesis: ( S is finite & S is monotonic & S is Circuit-like )
thus S is finite ; :: thesis: ( S is monotonic & S is Circuit-like )
thus S is monotonic :: thesis: S is Circuit-like
proof
reconsider S9 = S as non empty non void ManySortedSign ;
let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def 13 :: thesis:
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 V39() 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 ; :: according to FINSET_1:def 5,MSAFREE2:def 11 :: thesis: ( 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 V5() ManySortedSet of the carrier of S ;
assume i in the carrier of S ; :: thesis: the Sorts of A . i is finite
then A3: i = the SortSymbol of S9 by ;
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 :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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
.= (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 ;
( the OperSymbol of S9 .--> (Den ( the OperSymbol of S9,A9))) . i = Den ( the OperSymbol of S9,A9) by ;
then A9: rng Oi = {((Den ( the OperSymbol of S9,A9)) . {})} by ;
(T * the ResultSort of S) . i = T . ( the ResultSort of S . i) by
.= 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 ;
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; :: thesis: 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 ;
A11: now :: thesis: 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; :: thesis: ( 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 #) ; :: thesis: ( B is opers_closed & the Charact of MSAlgebra(# T,O #) = Opers (A9,B) )
thus A13: B is opers_closed :: thesis: the Charact of MSAlgebra(# T,O #) = Opers (A9,B)
proof
let o9 be OperSymbol of S9; :: according to MSUALG_2:def 6 :: thesis: B is_closed_on o9
let x be object ; :: according to TARSKI:def 3,MSUALG_2:def 5 :: thesis: ( 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)) ; :: thesis: x in ( the ResultSort of S9 * B) . o9
A15: o9 = the OperSymbol of S9 by ;
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 ;
then x = (Den ( the OperSymbol of S9,A9)) . {} by ;
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 ;
then x in B . the SortSymbol of S9 by ;
hence x in ( the ResultSort of S9 * B) . o9 by ; :: thesis: verum
end;
now :: thesis: for o9 being OperSymbol of S9 holds the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B
let o9 be OperSymbol of S9; :: thesis: the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B
((B #) * the Arity of S9) . the OperSymbol of S9 = (B #) . ( the Arity of S9 . the OperSymbol of S9) by FUNCT_2:15
.= (T #) . (<*> the carrier of S9) by A12
.= by PRE_CIRC:2 ;
then (Den ( the OperSymbol of S9,A9)) | (((B #) * the Arity of S9) . the OperSymbol of S9) = Den ( the OperSymbol of S9,A9) by A5;
then A19: the Charact of MSAlgebra(# T,O #) . the OperSymbol of S9 = (Den ( the OperSymbol of S9,A9)) | (((B #) * the Arity of S9) . the OperSymbol of S9) by FUNCOP_1:72;
( o9 = the OperSymbol of S9 & B is_closed_on the OperSymbol of S9 ) by ;
hence the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B by ; :: thesis: verum
end;
hence the Charact of MSAlgebra(# T,O #) = Opers (A9,B) by ; :: thesis: 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 ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S9 or T9 . i c= the Sorts of A9 . i )
assume i in the carrier of S9 ; :: thesis: 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 ;
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 ;
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 ;
hence T9 . i c= the Sorts of A9 . i by ; :: thesis: 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 ;
A24: now :: thesis: for U1 being MSSubAlgebra of A9 st G9 is MSSubset of U1 holds
A99 is MSSubAlgebra of U1
let U1 be MSSubAlgebra of A9; :: thesis: ( G9 is MSSubset of U1 implies A99 is MSSubAlgebra of U1 )
assume A25: G9 is MSSubset of U1 ; :: thesis: A99 is MSSubAlgebra of U1
now :: thesis: 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 ;
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 ;
let i be object ; :: thesis: ( 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 ;
then (Den ( the OperSymbol of S9,A9)) . {} in Constants (A9, the SortSymbol of S9) by ;
then A29: {((Den ( the OperSymbol of S9,A9)) . {})} c= the Sorts of U1 . the SortSymbol of S9 by ;
G c= the Sorts of U1 by ;
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 ; :: thesis: the Sorts of A99 . i c= the Sorts of U1 . i
then i = the SortSymbol of S9 by ;
hence the Sorts of A99 . i c= the Sorts of U1 . i by ; :: thesis: verum
end;
then the Sorts of A99 c= the Sorts of U1 ;
hence A99 is MSSubAlgebra of U1 by MSUALG_2:8; :: thesis: verum
end;
now :: thesis: for i being object st i in the carrier of S9 holds
G9 . i c= the Sorts of A99 . i
let i be object ; :: thesis: ( i in the carrier of S9 implies G9 . i c= the Sorts of A99 . i )
assume i in the carrier of S9 ; :: thesis: G9 . i c= the Sorts of A99 . i
then A31: i = the SortSymbol of S9 by ;
the Sorts of A99 . the SortSymbol of S9 = (G . the SortSymbol of S9) \/ {((Den ( the OperSymbol of S9,A9)) . {})} by FUNCOP_1:72;
hence G9 . i c= the Sorts of A99 . i by ; :: thesis: 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 () by
.= the Sorts of A9 by MSAFREE:def 4 ;
then the Sorts of A . i = Gs \/ {((Den ( the OperSymbol of S9,A9)) . {})} by ;
hence the Sorts of A . i is finite ; :: thesis: verum
end;
thus S is Circuit-like :: thesis: verum
proof
let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( S9 = S implies for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2 )

assume A32: S9 = S ; :: thesis: for o1, o2 being OperSymbol of S9 st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2

let o1, o2 be OperSymbol of S9; :: thesis: ( the_result_sort_of o1 = the_result_sort_of o2 implies o1 = o2 )
assume the_result_sort_of o1 = the_result_sort_of o2 ; :: thesis: o1 = o2
o1 = by ;
hence o1 = o2 by ; :: thesis: verum
end;