let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds the Sorts of A is GeneratorSet of A

let A be non-empty MSAlgebra over S; :: thesis: the Sorts of A is GeneratorSet of A

reconsider theA = MSAlgebra(# the Sorts of A, the Charact of A #) as non-empty MSAlgebra over S ;

reconsider AA = the Sorts of A as V5() MSSubset of theA by PBOOLE:def 18;

set GAA = GenMSAlg AA;

A1: the Sorts of (GenMSAlg AA) is MSSubset of A by MSUALG_2:def 9;

reconsider BB = the Sorts of A as MSSubset of A by PBOOLE:def 18;

then GenMSAlg AA = GenMSAlg BB by A8, MSUALG_2:def 17;

then the Sorts of (GenMSAlg BB) = the Sorts of A by MSUALG_2:21;

hence the Sorts of A is GeneratorSet of A by MSAFREE:def 4; :: thesis: verum

let A be non-empty MSAlgebra over S; :: thesis: the Sorts of A is GeneratorSet of A

reconsider theA = MSAlgebra(# the Sorts of A, the Charact of A #) as non-empty MSAlgebra over S ;

reconsider AA = the Sorts of A as V5() MSSubset of theA by PBOOLE:def 18;

set GAA = GenMSAlg AA;

A1: the Sorts of (GenMSAlg AA) is MSSubset of A by MSUALG_2:def 9;

now :: thesis: for B being MSSubset of A st B = the Sorts of (GenMSAlg AA) holds

( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) )

then reconsider GAA = GenMSAlg AA as strict non-empty MSSubAlgebra of A by A1, MSUALG_2:def 9;( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) )

let B be MSSubset of A; :: thesis: ( B = the Sorts of (GenMSAlg AA) implies ( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) ) )

assume A2: B = the Sorts of (GenMSAlg AA) ; :: thesis: ( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) )

reconsider C = B as MSSubset of theA ;

A3: C is opers_closed by A2, MSUALG_2:def 9;

reconsider OAB = Opers (A,B) as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S ;

hence the Charact of (GenMSAlg AA) = Opers (A,B) by A6, MSUALG_2:def 8; :: thesis: verum

end;assume A2: B = the Sorts of (GenMSAlg AA) ; :: thesis: ( B is opers_closed & the Charact of (GenMSAlg AA) = Opers (A,B) )

reconsider C = B as MSSubset of theA ;

A3: C is opers_closed by A2, MSUALG_2:def 9;

A4: now :: thesis: for o being OperSymbol of S holds B is_closed_on o

hence
B is opers_closed
; :: thesis: the Charact of (GenMSAlg AA) = Opers (A,B)let o be OperSymbol of S; :: thesis: B is_closed_on o

C is_closed_on o by A3;

then A5: rng ((Den (o,MSAlgebra(# the Sorts of A, the Charact of A #))) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o ;

thus B is_closed_on o by A5; :: thesis: verum

end;C is_closed_on o by A3;

then A5: rng ((Den (o,MSAlgebra(# the Sorts of A, the Charact of A #))) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o ;

thus B is_closed_on o by A5; :: thesis: verum

reconsider OAB = Opers (A,B) as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S ;

A6: now :: thesis: for o being OperSymbol of S holds OAB . o = o /. C

the Charact of (GenMSAlg AA) = Opers (theA,C)
by A2, MSUALG_2:def 9;let o be OperSymbol of S; :: thesis: OAB . o = o /. C

A7: ( C is_closed_on o & Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ) by A3;

thus OAB . o = o /. B by MSUALG_2:def 8

.= (Den (o,A)) | (((B #) * the Arity of S) . o) by A4, MSUALG_2:def 7

.= o /. C by A7, MSUALG_2:def 7 ; :: thesis: verum

end;A7: ( C is_closed_on o & Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ) by A3;

thus OAB . o = o /. B by MSUALG_2:def 8

.= (Den (o,A)) | (((B #) * the Arity of S) . o) by A4, MSUALG_2:def 7

.= o /. C by A7, MSUALG_2:def 7 ; :: thesis: verum

hence the Charact of (GenMSAlg AA) = Opers (A,B) by A6, MSUALG_2:def 8; :: thesis: verum

reconsider BB = the Sorts of A as MSSubset of A by PBOOLE:def 18;

A8: now :: thesis: for U1 being MSSubAlgebra of A st BB is MSSubset of U1 holds

GAA is MSSubAlgebra of U1

BB is MSSubset of (GenMSAlg AA)
by MSUALG_2:def 17;GAA is MSSubAlgebra of U1

let U1 be MSSubAlgebra of A; :: thesis: ( BB is MSSubset of U1 implies GAA is MSSubAlgebra of U1 )

then reconsider U2 = U1 as MSSubAlgebra of theA by A9, MSUALG_2:def 9;

assume BB is MSSubset of U1 ; :: thesis: GAA is MSSubAlgebra of U1

then GAA is MSSubAlgebra of U2 by MSUALG_2:def 17;

hence GAA is MSSubAlgebra of U1 ; :: thesis: verum

end;A9: now :: thesis: for B being MSSubset of theA st B = the Sorts of U1 holds

( B is opers_closed & the Charact of U1 = Opers (theA,B) )

the Sorts of U1 is MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #)
by MSUALG_2:def 9;( B is opers_closed & the Charact of U1 = Opers (theA,B) )

let B be MSSubset of theA; :: thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (theA,B) ) )

assume A10: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers (theA,B) )

reconsider C = B as MSSubset of A ;

A11: C is opers_closed by A10, MSUALG_2:def 9;

reconsider OAB = Opers (theA,B) as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S ;

hence the Charact of U1 = Opers (theA,B) by A14, MSUALG_2:def 8; :: thesis: verum

end;assume A10: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers (theA,B) )

reconsider C = B as MSSubset of A ;

A11: C is opers_closed by A10, MSUALG_2:def 9;

A12: now :: thesis: for o being OperSymbol of S holds B is_closed_on o

hence
B is opers_closed
; :: thesis: the Charact of U1 = Opers (theA,B)let o be OperSymbol of S; :: thesis: B is_closed_on o

C is_closed_on o by A11;

then A13: rng ((Den (o,A)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o ;

thus B is_closed_on o by A13; :: thesis: verum

end;C is_closed_on o by A11;

then A13: rng ((Den (o,A)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o ;

thus B is_closed_on o by A13; :: thesis: verum

reconsider OAB = Opers (theA,B) as ManySortedFunction of (C #) * the Arity of S,C * the ResultSort of S ;

A14: now :: thesis: for o being OperSymbol of S holds OAB . o = o /. C

the Charact of U1 = Opers (A,C)
by A10, MSUALG_2:def 9;let o be OperSymbol of S; :: thesis: OAB . o = o /. C

A15: Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ;

A16: C is_closed_on o by A11;

thus OAB . o = o /. B by MSUALG_2:def 8

.= (Den (o,A)) | (((B #) * the Arity of S) . o) by A12, A15, MSUALG_2:def 7

.= o /. C by A16, MSUALG_2:def 7 ; :: thesis: verum

end;A15: Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ;

A16: C is_closed_on o by A11;

thus OAB . o = o /. B by MSUALG_2:def 8

.= (Den (o,A)) | (((B #) * the Arity of S) . o) by A12, A15, MSUALG_2:def 7

.= o /. C by A16, MSUALG_2:def 7 ; :: thesis: verum

hence the Charact of U1 = Opers (theA,B) by A14, MSUALG_2:def 8; :: thesis: verum

then reconsider U2 = U1 as MSSubAlgebra of theA by A9, MSUALG_2:def 9;

assume BB is MSSubset of U1 ; :: thesis: GAA is MSSubAlgebra of U1

then GAA is MSSubAlgebra of U2 by MSUALG_2:def 17;

hence GAA is MSSubAlgebra of U1 ; :: thesis: verum

then GenMSAlg AA = GenMSAlg BB by A8, MSUALG_2:def 17;

then the Sorts of (GenMSAlg BB) = the Sorts of A by MSUALG_2:21;

hence the Sorts of A is GeneratorSet of A by MSAFREE:def 4; :: thesis: verum