let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
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 #) & A is X,S -terms holds
B is X,S -terms
let X be V5() ManySortedSet of S; :: 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 #) & A is X,S -terms holds
B is X,S -terms
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 #) & A is X,S -terms implies B is X,S -terms )
assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: ( not A is X,S -terms or B is X,S -terms )
assume A2: ( the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) & FreeGen X is ManySortedSubset of the Sorts of A & ( for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) ) & ( for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G ) ) ) ; :: according to MSAFREE4:def 6 :: thesis: B is X,S -terms
hence ( the Sorts of B is ManySortedSubset of the Sorts of (Free (S,X)) & FreeGen X is ManySortedSubset of the Sorts of B ) by A1; :: according to MSAFREE4:def 6 :: thesis: ( ( for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) holds
( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) ) & ( for f being ManySortedFunction of FreeGen X, the Sorts of B
for G being ManySortedSubset of the Sorts of B st G = FreeGen X holds
ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G ) ) )

hereby :: thesis: for f being ManySortedFunction of FreeGen X, the Sorts of B
for G being ManySortedSubset of the Sorts of B st G = FreeGen X holds
ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G )

let o be OperSymbol of S; :: thesis: for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) holds
( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p )
let p be FinSequence; :: thesis: ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) implies ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) )
( Args (o,A) = Args (o,B) & Den (o,A) = Den (o,B) ) by A1;
hence ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) implies ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) ) by A1, A2; :: thesis: verum

end;

let f be ManySortedFunction of FreeGen X, the Sorts of B; :: thesis: for G being ManySortedSubset of the Sorts of B st G = FreeGen X holds
ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G )
let G be ManySortedSubset of the Sorts of B; :: thesis: ( G = FreeGen X implies ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G ) )
assume A3: G = FreeGen X ; :: thesis: ex h being ManySortedFunction of B,B st
( h is_homomorphism B,B & f = h || G )
reconsider G1 = G as ManySortedSubset of the Sorts of A by A1;
consider h being ManySortedFunction of A,A such that
A4: ( h is_homomorphism A,A & f = h || G1 ) by A1, A2, A3;
reconsider h2 = h as ManySortedFunction of B,B by A1;
take h2 ; :: thesis: ( h2 is_homomorphism B,B & f = h2 || G )
thus h2 is_homomorphism B,B by A4, A1, Th30; :: thesis: f = h2 || G
thus f = h2 || G by A1, A4; :: thesis: verum