let S be non empty non void ManySortedSign ; 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; ( 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 #)
; 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; for H being MSSubset of B st G = H holds
GenMSAlg G = GenMSAlg H
let H be MSSubset of B; ( G = H implies GenMSAlg G = GenMSAlg H )
assume A2:
G = H
; 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; verum