let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S holds the Sorts of A is GeneratorSet of A
let A be non-empty MSAlgebra of 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 of S ;
reconsider AA = the Sorts of A as V16() MSSubset of theA by PBOOLE:def 23;
set GAA = GenMSAlg AA;
A1: the Sorts of (GenMSAlg AA) is MSSubset of A by MSUALG_2:def 10;

now

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

A4: now

let o be OperSymbol of S; :: thesis: B is_closed_on o
C is_closed_on o by A3, MSUALG_2:def 7;
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 by MSUALG_2:def 6;
Den (o,A) = Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) ;
hence B is_closed_on o by A5, MSUALG_2:def 6; :: thesis: verum

end;

hence B is opers_closed by MSUALG_2:def 7; :: 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

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, MSUALG_2:def 7;
thus OAB . o = o /. B by MSUALG_2:def 9
.= (Den (o,A)) | (((B #) * the Arity of S) . o) by A4, MSUALG_2:def 8
.= o /. C by A7, MSUALG_2:def 8 ; :: thesis: verum

end;

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

end;

then reconsider GAA = GenMSAlg AA as strict non-empty MSSubAlgebra of A by A1, MSUALG_2:def 10;
reconsider BB = the Sorts of A as MSSubset of A by PBOOLE:def 23;

A8: now

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

A9: now

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

A12: now

let o be OperSymbol of S; :: thesis: B is_closed_on o
C is_closed_on o by A11, MSUALG_2:def 7;
then A13: rng ((Den (o,A)) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o by MSUALG_2:def 6;
Den (o,MSAlgebra(# the Sorts of A, the Charact of A #)) = Den (o,A) ;
hence B is_closed_on o by A13, MSUALG_2:def 6; :: thesis: verum

end;

hence B is opers_closed by MSUALG_2:def 7; :: 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

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, MSUALG_2:def 7;
thus OAB . o = o /. B by MSUALG_2:def 9
.= (Den (o,A)) | (((B #) * the Arity of S) . o) by A12, A15, MSUALG_2:def 8
.= o /. C by A16, MSUALG_2:def 8 ; :: thesis: verum

end;

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

end;

the Sorts of U1 is MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:def 10;
then reconsider U2 = U1 as MSSubAlgebra of theA by A9, MSUALG_2:def 10;
assume BB is MSSubset of U1 ; :: thesis: GAA is MSSubAlgebra of U1
then GAA is MSSubAlgebra of U2 by MSUALG_2:def 18;
hence GAA is MSSubAlgebra of U1 ; :: thesis: verum

end;

BB is MSSubset of (GenMSAlg AA) by MSUALG_2:def 18;
then GenMSAlg AA = GenMSAlg BB by A8, MSUALG_2:def 18;
then the Sorts of (GenMSAlg BB) = the Sorts of A by MSUALG_2:22;
hence the Sorts of A is GeneratorSet of A by MSAFREE:def 4; :: thesis: verum