let S be non void feasible ManySortedSign ; :: thesis: for S' being non void Subsignature of S
for A1, A2 being MSAlgebra of S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,(A1 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' )
let S' be non void Subsignature of S; :: thesis: for A1, A2 being MSAlgebra of S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,(A1 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' )
let A1, A2 be MSAlgebra of S; :: thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,(A1 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' ) )
assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; :: thesis: for h being ManySortedFunction of ,A1 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of ,(A1 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' )
set f = id the carrier of S';
set g = id the carrier' of S';
A2: id the carrier of S', id the carrier' of S' form_morphism_between S',S by Def2;
then reconsider f = id the carrier of S' as Function of the carrier of S',the carrier of S by Th10;
let h be ManySortedFunction of ,A1; :: thesis: ( h is_homomorphism A1,A2 implies ex h' being ManySortedFunction of ,(A1 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' ) )
assume h is_homomorphism A1,A2 ; :: thesis: ex h' being ManySortedFunction of ,(A1 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' )
then consider h' being ManySortedFunction of ,(A1 | S',f,(id the carrier' of S')) such that
A3: h' = h * f and
A4: h' is_homomorphism A1 | S',f,(id the carrier' of S'),A2 | S',f,(id the carrier' of S') by A1, A2, Th35;
consider k being ManySortedFunction of ,(A1 | S') such that
A5: k = h' and
k is_homomorphism A1 | S',A2 | S' by A4;
take k ; :: thesis: ( k = h | the carrier of S' & k is_homomorphism A1 | S',A2 | S' )
thus ( k = h | the carrier of S' & k is_homomorphism A1 | S',A2 | S' ) by A3, A4, A5, RELAT_1:94; :: thesis: verum