let S be non empty non void ManySortedSign ; :: thesis:
let A, B be non-empty MSAlgebra over S; :: thesis:
let F be ManySortedFunction of A,B; :: thesis:
assume A1: F is_homomorphism A,B ; :: thesis:
MSHomQuot F is_monomorphism QuotMSAlg (A,(MSCng F)),B by A1, MSUALG_4:4;
then A2: MSHomQuot F is_homomorphism QuotMSAlg (A,(MSCng F)),B ;
let C1 be MSCongruence of A; :: thesis:
assume A3: C1 c= MSCng F ; :: thesis:
set G = MSNat_Hom (A,C1);
set I = the carrier of S;
set sQ = the Sorts of (QuotMSAlg (A,C1));
set sF = the Sorts of (QuotMSAlg (A,(MSCng F)));
defpred S₁[ object , object , object ] means ex s being Element of the carrier of S ex xx being Element of the Sorts of A . s st
( $3 = s & $2 = Class (C1,xx) & $1 = Class ((MSCng F),xx) );
A4: for i being object st i in the carrier of S holds
for x being object st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
ex y being object st
( y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i & S₁[y,x,i] )

let i be object ; :: thesis:
assume i in the carrier of S ; :: thesis:
then reconsider s = i as Element of the carrier of S ;
let x be object ; :: thesis:
assume x in the Sorts of (QuotMSAlg (A,C1)) . i ; :: thesis:
then consider x1 being Element of the Sorts of A . s such that
A5: x = Class (C1,x1) by Th31;
take y = Class ((MSCng F),x1); :: thesis:
y in Class ((MSCng F) . s) by EQREL_1:def 3;
hence y in the Sorts of (QuotMSAlg (A,(MSCng F))) . i by MSUALG_4:def 6; :: thesis:
thus S₁[y,x,i] by A5; :: thesis:

end;

consider C12 being ManySortedFunction of the Sorts of (QuotMSAlg (A,C1)), the Sorts of (QuotMSAlg (A,(MSCng F))) such that
A6: for i being object st i in the carrier of S holds
ex f being Function of ( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i) st
( f = C12 . i & ( for x being object st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
S₁[f . x,x,i] ) ) from MSSUBFAM:sch 1(A4);
reconsider H = (MSHomQuot F) ** C12 as ManySortedFunction of (QuotMSAlg (A,C1)),B ;
take H ; :: thesis:
A7: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg (A,C1)) . i
for xx being Element of the Sorts of A . i st x = Class (C1,xx) holds
(C12 . i) . x = Class ((MSCng F),xx)

let i be Element of S; :: thesis:
let x be Element of the Sorts of (QuotMSAlg (A,C1)) . i; :: thesis:
let xx be Element of the Sorts of A . i; :: thesis:
assume A8: x = Class (C1,xx) ; :: thesis:
consider f being Function of ( the Sorts of (QuotMSAlg (A,C1)) . i),( the Sorts of (QuotMSAlg (A,(MSCng F))) . i) such that
A9: f = C12 . i and
A10: for x being object st x in the Sorts of (QuotMSAlg (A,C1)) . i holds
S₁[f . x,x,i] by A6;
consider s being Element of the carrier of S, x1 being Element of the Sorts of A . s such that
A11: i = s and
A12: x = Class (C1,x1) and
A13: f . x = Class ((MSCng F),x1) by A10;
xx in Class ((C1 . s),x1) by A8, A12, EQREL_1:23;
then A14: [xx,x1] in C1 . s by EQREL_1:19;
C1 . s c= (MSCng F) . s by A3;
then xx in Class (((MSCng F) . s),x1) by A14, EQREL_1:19;
hence (C12 . i) . x = Class ((MSCng F),xx) by A9, A11, A13, EQREL_1:23; :: thesis:

end;

let i be object ; :: thesis:
assume i in the carrier of S ; :: thesis:
then reconsider s = i as SortSymbol of S ;
A16: for x being Element of the Sorts of A . s holds ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = ((MSNat_Hom (A,(MSCng F))) . s) . x

let x be Element of the Sorts of A . s; :: thesis:
Class ((C1 . s),x) in Class (C1 . s) by EQREL_1:def 3;
then A17: Class (C1,x) in (Class C1) . s by MSUALG_4:def 6;
thus ((C12 . s) * ((MSNat_Hom (A,C1)) . s)) . x = (C12 . s) . (((MSNat_Hom (A,C1)) . s) . x) by FUNCT_2:15
.= (C12 . s) . ((MSNat_Hom (A,C1,s)) . x) by MSUALG_4:def 16
.= (C12 . s) . (Class (C1,x)) by MSUALG_4:def 15
.= Class ((MSCng F),x) by A7, A17
.= (MSNat_Hom (A,(MSCng F),s)) . x by MSUALG_4:def 15
.= ((MSNat_Hom (A,(MSCng F))) . s) . x by MSUALG_4:def 16 ; :: thesis:

end;

thus (C12 ** (MSNat_Hom (A,C1))) . i = (C12 . s) * ((MSNat_Hom (A,C1)) . s) by MSUALG_3:2
.= (MSNat_Hom (A,(MSCng F))) . i by A16, FUNCT_2:63 ; :: thesis:

end;