let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty MSAlgebra over 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 over 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 :: thesis: for i being object st i in the carrier of S holds
((MSHomQuot F) ** (MSNat_Hom (A,(MSCng F)))) . i = F . i

let i be object ; :: 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:15
.= h . (Class (((MSCng F) . s),c)) by MSUALG_4:def 15
.= h . (Class ((MSCng (F,s)),c)) by A1, MSUALG_4:def 18
.= (F . s) . c by A1, MSUALG_4:def 19 ; :: 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 20
.= (MSHomQuot (F,s)) * (MSNat_Hom (A,(MSCng F),s)) by MSUALG_4:def 16
.= F . i by A2, FUNCT_2:63 ; :: thesis: verum

end;

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