let S be non empty non void ManySortedSign ; :: thesis: for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for G being MSSubset of A
for H being MSSubset of B st G = H holds
GenMSAlg G = GenMSAlg H
let A, B be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) implies for G being MSSubset of A
for H being MSSubset of B st G = H holds
GenMSAlg G = GenMSAlg H )
assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: for G being MSSubset of A
for H being MSSubset of B st G = H holds
GenMSAlg G = GenMSAlg H
let G be MSSubset of A; :: thesis: for H being MSSubset of B st G = H holds
GenMSAlg G = GenMSAlg H
let H be MSSubset of B; :: thesis: ( G = H implies GenMSAlg G = GenMSAlg H )
assume A2: G = H ; :: thesis: GenMSAlg G = GenMSAlg H
A3: ( G is MSSubset of (GenMSAlg G) & H is MSSubset of (GenMSAlg H) ) by MSUALG_2:def 17;
( GenMSAlg G is MSSubAlgebra of B & GenMSAlg H is MSSubAlgebra of A ) by A1, MSAFREE4:28;
then ( GenMSAlg G is MSSubAlgebra of GenMSAlg H & GenMSAlg H is MSSubAlgebra of GenMSAlg G ) by A2, A3, MSUALG_2:def 17;
hence GenMSAlg G = GenMSAlg H by MSUALG_2:7; :: thesis: verum