let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty 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 GeneratorSet of A

for H being GeneratorSet of B st G = H & G is free holds

H is free

let A, B be non-empty 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 GeneratorSet of A

for H being GeneratorSet of B st G = H & G is free holds

H is free )

assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: for G being GeneratorSet of A

for H being GeneratorSet of B st G = H & G is free holds

H is free

let G be GeneratorSet of A; :: thesis: for H being GeneratorSet of B st G = H & G is free holds

H is free

let H be GeneratorSet of B; :: thesis: ( G = H & G is free implies H is free )

assume A2: G = H ; :: thesis: ( not G is free or H is free )

assume A3: for U1 being non-empty MSAlgebra over S

for f being ManySortedFunction of G, the Sorts of U1 ex h being ManySortedFunction of A,U1 st

( h is_homomorphism A,U1 & h || G = f ) ; :: according to MSAFREE:def 5 :: thesis: H is free

let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def 5 :: thesis: for b_{1} being ManySortedFunction of H, the Sorts of U1 ex b_{2} being ManySortedFunction of the Sorts of B, the Sorts of U1 st

( b_{2} is_homomorphism B,U1 & b_{2} || H = b_{1} )

let f be ManySortedFunction of H, the Sorts of U1; :: thesis: ex b_{1} being ManySortedFunction of the Sorts of B, the Sorts of U1 st

( b_{1} is_homomorphism B,U1 & b_{1} || H = f )

consider h being ManySortedFunction of A,U1 such that

A4: ( h is_homomorphism A,U1 & h || G = f ) by A2, A3;

reconsider g = h as ManySortedFunction of B,U1 by A1;

take g ; :: thesis: ( g is_homomorphism B,U1 & g || H = f )

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) ;

hence g is_homomorphism B,U1 by A1, A4, MSAFREE4:30; :: thesis: g || H = f

thus g || H = f by A1, A2, A4; :: thesis: verum

for G being GeneratorSet of A

for H being GeneratorSet of B st G = H & G is free holds

H is free

let A, B be non-empty 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 GeneratorSet of A

for H being GeneratorSet of B st G = H & G is free holds

H is free )

assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: for G being GeneratorSet of A

for H being GeneratorSet of B st G = H & G is free holds

H is free

let G be GeneratorSet of A; :: thesis: for H being GeneratorSet of B st G = H & G is free holds

H is free

let H be GeneratorSet of B; :: thesis: ( G = H & G is free implies H is free )

assume A2: G = H ; :: thesis: ( not G is free or H is free )

assume A3: for U1 being non-empty MSAlgebra over S

for f being ManySortedFunction of G, the Sorts of U1 ex h being ManySortedFunction of A,U1 st

( h is_homomorphism A,U1 & h || G = f ) ; :: according to MSAFREE:def 5 :: thesis: H is free

let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def 5 :: thesis: for b

( b

let f be ManySortedFunction of H, the Sorts of U1; :: thesis: ex b

( b

consider h being ManySortedFunction of A,U1 such that

A4: ( h is_homomorphism A,U1 & h || G = f ) by A2, A3;

reconsider g = h as ManySortedFunction of B,U1 by A1;

take g ; :: thesis: ( g is_homomorphism B,U1 & g || H = f )

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) ;

hence g is_homomorphism B,U1 by A1, A4, MSAFREE4:30; :: thesis: g || H = f

thus g || H = f by A1, A2, A4; :: thesis: verum