{} 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

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

thus
S is Circuit-like
:: thesis: verum
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: 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 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 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;

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;

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

then reconsider A99 = A99 as strict MSSubAlgebra of A9 by A11, MSUALG_2:def 9;

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 ; :: thesis: verum

end;let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def 13 :: thesis: 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 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 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 :: 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)

A10:
the OperSymbol of S9 = [{},{{}}]
by TARSKI:def 1;( 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 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; :: thesis: verum

end;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 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; :: thesis: verum

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 :: 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) )

reconsider A99 = MSAlgebra(# T,O #) as non-empty MSAlgebra over S9 by MSUALG_1:def 3;( 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)

end;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 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; :: thesis: verum

end;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 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; :: thesis: verum

now :: thesis: for o9 being OperSymbol of S9 holds the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B

hence
the Charact of MSAlgebra(# T,O #) = Opers (A9,B)
by A12, MSUALG_2:def 8; :: thesis: verumlet 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 A10, A13, TARSKI:def 1;

hence the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B by A19, MSUALG_2:def 7; :: thesis: verum

end;((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 A10, A13, TARSKI:def 1;

hence the Charact of MSAlgebra(# T,O #) . o9 = o9 /. B by A19, MSUALG_2:def 7; :: thesis: verum

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

then
the Sorts of MSAlgebra(# T,O #) is MSSubset of A9
by PBOOLE:def 18;
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 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; :: thesis: verum

end;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 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; :: thesis: verum

then reconsider A99 = A99 as strict MSSubAlgebra of A9 by A11, MSUALG_2:def 9;

A24: now :: thesis: for U1 being MSSubAlgebra of A9 st G9 is MSSubset of U1 holds

A99 is MSSubAlgebra of U1

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

hence A99 is MSSubAlgebra of U1 by MSUALG_2:8; :: thesis: verum

end;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

then
the Sorts of A99 c= the Sorts of U1
;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 ; :: 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 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 ; :: thesis: the Sorts of A99 . i c= the Sorts of U1 . i

then 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; :: thesis: verum

end;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 ; :: 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 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 ; :: thesis: the Sorts of A99 . i c= the Sorts of U1 . i

then 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; :: thesis: verum

hence A99 is MSSubAlgebra of U1 by MSUALG_2:8; :: thesis: verum

now :: thesis: for i being object st i in the carrier of S9 holds

G9 . i c= the Sorts of A99 . i

then
G9 c= the Sorts of A99
;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 A2, TARSKI:def 1;

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 A31, XBOOLE_1:7; :: thesis: verum

end;assume i in the carrier of S9 ; :: thesis: G9 . i c= the Sorts of A99 . i

then A31: i = the SortSymbol of S9 by A2, TARSKI:def 1;

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 A31, XBOOLE_1:7; :: thesis: verum

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 ; :: 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 A32, TARSKI:def 1;

hence o1 = o2 by A32, TARSKI:def 1; :: thesis: verum

end;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 A32, TARSKI:def 1;

hence o1 = o2 by A32, TARSKI:def 1; :: thesis: verum