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,A2 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of (A1 | S'),(A2 | 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,A2 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of (A1 | S'),(A2 | 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,A2 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of (A1 | S'),(A2 | 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,A2 st h is_homomorphism A1,A2 holds
ex h' being ManySortedFunction of (A1 | S'),(A2 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' )
let h be ManySortedFunction of A1,A2; :: thesis: ( h is_homomorphism A1,A2 implies ex h' being ManySortedFunction of (A1 | S'),(A2 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' ) )
assume A2: h is_homomorphism A1,A2 ; :: thesis: ex h' being ManySortedFunction of (A1 | S'),(A2 | 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';
A3: 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;
consider h' being ManySortedFunction of (A1 | S',f,(id the carrier' of S')),(A2 | S',f,(id the carrier' of S')) such that
A4: ( h' = h * f & h' is_homomorphism A1 | S',f,(id the carrier' of S'),A2 | S',f,(id the carrier' of S') ) by A1, A2, A3, Th35;
consider k being ManySortedFunction of (A1 | S'),(A2 | S') such that
A5: ( k = h' & 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 A4, A5, RELAT_1:94; :: thesis: verum