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 non-empty 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) )

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;

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

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;

hence B is opers_closed ; :: thesis: the Charact of (GenMSAlg AA) = Opers (A,B)
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

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;

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

end;

then reconsider GAA = GenMSAlg AA as strict non-empty MSSubAlgebra of A by A1, MSUALG_2:def 9;
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

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

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

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;

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

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;

hence B is opers_closed ; :: thesis: the Charact of U1 = Opers (theA,B)
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

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;

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

end;

the Sorts of U1 is MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:def 9;
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;

BB is MSSubset of (GenMSAlg AA) by MSUALG_2:def 17;
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