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