theorem Th14: :: EXTENS_1:14

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for X being non-empty ManySortedSet of the carrier of S
for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds
h1 = h2