let S be non void feasible ManySortedSign ; :: thesis: for S9 being non void Subsignature of S

for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds

for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

let S9 be non void Subsignature of S; :: thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds

for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

let A1, A2 be MSAlgebra over S; :: thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) )

assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; :: thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

set f = id the carrier of S9;

set g = id the carrier' of S9;

A2: id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S by Def2;

then reconsider f = id the carrier of S9 as Function of the carrier of S9, the carrier of S by Th9;

let h be ManySortedFunction of A1,A2; :: thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) )

assume h is_homomorphism A1,A2 ; :: thesis: ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

then consider h9 being ManySortedFunction of (A1 | (S9,f,(id the carrier' of S9))),(A2 | (S9,f,(id the carrier' of S9))) such that

A3: h9 = h * f and

A4: h9 is_homomorphism A1 | (S9,f,(id the carrier' of S9)),A2 | (S9,f,(id the carrier' of S9)) by A1, A2, Th34;

consider k being ManySortedFunction of (A1 | S9),(A2 | S9) such that

A5: k = h9 and

k is_homomorphism A1 | S9,A2 | S9 by A4;

take k ; :: thesis: ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 )

thus ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 ) by A3, A4, A5, RELAT_1:65; :: thesis: verum

for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds

for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

let S9 be non void Subsignature of S; :: thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds

for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

let A1, A2 be MSAlgebra over S; :: thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) )

assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; :: thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds

ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

set f = id the carrier of S9;

set g = id the carrier' of S9;

A2: id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S by Def2;

then reconsider f = id the carrier of S9 as Function of the carrier of S9, the carrier of S by Th9;

let h be ManySortedFunction of A1,A2; :: thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) )

assume h is_homomorphism A1,A2 ; :: thesis: ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

then consider h9 being ManySortedFunction of (A1 | (S9,f,(id the carrier' of S9))),(A2 | (S9,f,(id the carrier' of S9))) such that

A3: h9 = h * f and

A4: h9 is_homomorphism A1 | (S9,f,(id the carrier' of S9)),A2 | (S9,f,(id the carrier' of S9)) by A1, A2, Th34;

consider k being ManySortedFunction of (A1 | S9),(A2 | S9) such that

A5: k = h9 and

k is_homomorphism A1 | S9,A2 | S9 by A4;

take k ; :: thesis: ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 )

thus ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 ) by A3, A4, A5, RELAT_1:65; :: thesis: verum