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₁ being ManySortedFunction of H, the Sorts of U1 ex b₂ being ManySortedFunction of the Sorts of B, the Sorts of U1 st
( b₂ is_homomorphism B,U1 & b₂ || H = b₁ )
let f be ManySortedFunction of H, the Sorts of U1; :: thesis: ex b₁ being ManySortedFunction of the Sorts of B, the Sorts of U1 st
( b₁ is_homomorphism B,U1 & b₁ || 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