let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over S
for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
let A, B be non-empty MSAlgebra over S; :: thesis: for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
let C be non-empty MSSubAlgebra of A; :: thesis: for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
let h1 be ManySortedFunction of B,C; :: thesis: ( h1 is_homomorphism B,C implies for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A )
assume A1: h1 is_homomorphism B,C ; :: thesis: for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
the Sorts of C is ManySortedSubset of the Sorts of A by MSUALG_2:def 9;
then id the Sorts of C is ManySortedFunction of C,A by EXTENS_1:5;
then consider G being ManySortedFunction of C,A such that
A2: G = id the Sorts of C ;
G is_monomorphism C,A by A2, MSUALG_3:22;
then A3: G is_homomorphism C,A ;
A4: G ** h1 = h1 by A2, MSUALG_3:4;
let h2 be ManySortedFunction of B,A; :: thesis: ( h1 = h2 implies h2 is_homomorphism B,A )
assume h1 = h2 ; :: thesis: h2 is_homomorphism B,A
hence h2 is_homomorphism B,A by A1, A4, A3, MSUALG_3:10; :: thesis: verum