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

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