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;
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 ;
A4: now :: thesis: for o being OperSymbol of S holds B is_closed_on o
let o be OperSymbol of S; :: thesis:
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
.= o /. C by ; :: thesis: verum
end;
the Charact of (GenMSAlg AA) = Opers (theA,C) by ;
hence the Charact of (GenMSAlg AA) = Opers (A,B) by ; :: thesis: verum
end;
then reconsider GAA = GenMSAlg AA as strict non-empty MSSubAlgebra of A by ;
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 ;
A12: now :: thesis: for o being OperSymbol of S holds B is_closed_on o
let o be OperSymbol of S; :: thesis:
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
.= o /. C by ; :: thesis: verum
end;
the Charact of U1 = Opers (A,C) by ;
hence the Charact of U1 = Opers (theA,B) by ; :: 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 ;
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 ;
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