let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra of S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom A,(MSCng F)) = F
let A, B be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom A,(MSCng F)) = F
let F be ManySortedFunction of A,B; :: thesis: ( F is_homomorphism A,B implies (MSHomQuot F) ** (MSNat_Hom A,(MSCng F)) = F )
assume A1: F is_homomorphism A,B ; :: thesis: (MSHomQuot F) ** (MSNat_Hom A,(MSCng F)) = F

now

let i be set ; :: thesis: ( i in the carrier of S implies ((MSHomQuot F) ** (MSNat_Hom A,(MSCng F))) . i = F . i )
assume i in the carrier of S ; :: thesis: ((MSHomQuot F) ** (MSNat_Hom A,(MSCng F))) . i = F . i
then reconsider s = i as SortSymbol of S ;
reconsider h = MSHomQuot F,s as Function of ((Class (MSCng F)) . s),(the Sorts of B . s) ;
reconsider f = h * (MSNat_Hom A,(MSCng F),s) as Function of (the Sorts of A . s),(the Sorts of B . s) ;
A2: for c being Element of the Sorts of A . s holds f . c = (F . s) . c

proof

let c be Element of the Sorts of A . s; :: thesis: f . c = (F . s) . c
thus f . c = h . ((MSNat_Hom A,(MSCng F),s) . c) by FUNCT_2:21
.= h . (Class ((MSCng F) . s),c) by MSUALG_4:def 17
.= h . (Class (MSCng F,s),c) by A1, MSUALG_4:def 20
.= (F . s) . c by A1, MSUALG_4:def 21 ; :: thesis: verum

end;

thus ((MSHomQuot F) ** (MSNat_Hom A,(MSCng F))) . i = ((MSHomQuot F) . s) * ((MSNat_Hom A,(MSCng F)) . s) by MSUALG_3:2
.= (MSHomQuot F,s) * ((MSNat_Hom A,(MSCng F)) . s) by MSUALG_4:def 22
.= (MSHomQuot F,s) * (MSNat_Hom A,(MSCng F),s) by MSUALG_4:def 18
.= F . i by A2, FUNCT_2:113 ; :: thesis: verum

end;

hence (MSHomQuot F) ** (MSNat_Hom A,(MSCng F)) = F by PBOOLE:3; :: thesis: verum