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 V5() MSSubset of theA by PBOOLE:def 23;
reconsider BB = the Sorts of A as MSSubset of A 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
A6: the Charact of (GenMSAlg AA) = Opers theA,C by A2, MSUALG_2:def 10;
reconsider OAB = Opers A,B as ManySortedFunction of (C # ) * the Arity of S,C * the ResultSort of S ;

now

let o be OperSymbol of S; :: thesis: OAB . o = o /. C
A7: C is_closed_on o by A3, MSUALG_2:def 7;
A8: Den o,A = Den o,MSAlgebra(# the Sorts of A,the Charact of A #) ;
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, A8, MSUALG_2:def 8 ; :: thesis: verum

end;

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

now

let U1 be MSSubAlgebra of A; :: thesis: ( BB is MSSubset of U1 implies GAA is MSSubAlgebra of U1 )
assume A10: BB is MSSubset of U1 ; :: thesis: GAA is MSSubAlgebra of U1
A11: the Sorts of U1 is MSSubset of MSAlgebra(# the Sorts of A,the Charact of A #) by MSUALG_2:def 10;

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 A12: B = the Sorts of U1 ; :: thesis: ( B is opers_closed & the Charact of U1 = Opers theA,B )
reconsider C = B as MSSubset of A ;
A13: C is opers_closed by A12, MSUALG_2:def 10;

A14: now

let o be OperSymbol of S; :: thesis: B is_closed_on o
C is_closed_on o by A13, MSUALG_2:def 7;
then A15: 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 A15, 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
A16: the Charact of U1 = Opers A,C by A12, MSUALG_2:def 10;
reconsider OAB = Opers theA,B as ManySortedFunction of (C # ) * the Arity of S,C * the ResultSort of S ;

now

let o be OperSymbol of S; :: thesis: OAB . o = o /. C
A17: C is_closed_on o by A13, MSUALG_2:def 7;
A18: Den o,A = Den o,MSAlgebra(# the Sorts of A,the Charact of A #) ;
thus OAB . o = o /. B by MSUALG_2:def 9
.= (Den o,A) | (((B # ) * the Arity of S) . o) by A14, A18, MSUALG_2:def 8
.= o /. C by A17, MSUALG_2:def 8 ; :: thesis: verum

end;

hence the Charact of U1 = Opers theA,B by A16, MSUALG_2:def 9; :: thesis: verum

end;

then reconsider U2 = U1 as MSSubAlgebra of theA by A11, MSUALG_2:def 10;
GAA is MSSubAlgebra of U2 by A10, MSUALG_2:def 18;
hence GAA is MSSubAlgebra of U1 ; :: thesis: verum

end;

then GenMSAlg AA = GenMSAlg BB by A9, 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