let U1 be Universal_Algebra; :: thesis: for E being Congruence of U1 holds Nat_Hom (U1,E) is_homomorphism
let E be Congruence of U1; :: thesis: Nat_Hom (U1,E) is_homomorphism
set f = Nat_Hom (U1,E);
set u1 = the carrier of U1;
set qu = the carrier of (QuotUnivAlg (U1,E));
A1: len (signature U1) = len the charact of U1 by UNIALG_1:def 4;
A2: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def 3;
A3: len (QuotOpSeq (U1,E)) = len the charact of U1 by Def9;
A4: len (signature (QuotUnivAlg (U1,E))) = len the charact of (QuotUnivAlg (U1,E)) by UNIALG_1:def 4;

now :: thesis: for n being Nat st n in dom (signature U1) holds
(signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n

let n be Nat; :: thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n )
assume A5: n in dom (signature U1) ; :: thesis: (signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n
then n in dom the charact of U1 by A1, A2, FINSEQ_1:def 3;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def 3;
n in dom (QuotOpSeq (U1,E)) by A3, A1, A2, A5, FINSEQ_1:def 3;
then A6: (QuotOpSeq (U1,E)) . n = QuotOp (o1,E) by Def9;
reconsider cl = QuotOp (o1,E) as non empty homogeneous quasi_total PartFunc of ( the carrier of (QuotUnivAlg (U1,E)) *), the carrier of (QuotUnivAlg (U1,E)) ;
consider b being object such that
A7: b in dom cl by XBOOLE_0:def 1;
reconsider b = b as Element of the carrier of (QuotUnivAlg (U1,E)) * by A7;
dom (QuotOp (o1,E)) = (arity o1) -tuples_on (Class E) by Def8;
then b in { w where w is Element of (Class E) * : len w = arity o1 } by A7, FINSEQ_2:def 4;
then ex w being Element of (Class E) * st
( w = b & len w = arity o1 ) ;
then A8: arity cl = arity o1 by A7, MARGREL1:def 25;
( n in dom (signature (QuotUnivAlg (U1,E))) & (signature U1) . n = arity o1 ) by A3, A4, A2, A5, FINSEQ_1:def 3, UNIALG_1:def 4;
hence (signature U1) . n = (signature (QuotUnivAlg (U1,E))) . n by A6, A8, UNIALG_1:def 4; :: thesis: verum

end;

hence signature U1 = signature (QuotUnivAlg (U1,E)) by A3, A4, A1, FINSEQ_2:9; :: according to UNIALG_2:def 1,ALG_1:def 1 :: thesis: for n being Nat st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
let n be Nat; :: thesis: ( n in dom the charact of U1 implies for o1 being operation of U1
for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) )
assume n in dom the charact of U1 ; :: thesis: for o1 being operation of U1
for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
then n in Seg (len the charact of U1) by FINSEQ_1:def 3;
then A9: n in dom (QuotOpSeq (U1,E)) by A3, FINSEQ_1:def 3;
let o1 be operation of U1; :: thesis: for o2 being operation of (QuotUnivAlg (U1,E)) st o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n holds
for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
let o2 be operation of (QuotUnivAlg (U1,E)); :: thesis: ( o1 = the charact of U1 . n & o2 = the charact of (QuotUnivAlg (U1,E)) . n implies for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) )
assume ( the charact of U1 . n = o1 & o2 = the charact of (QuotUnivAlg (U1,E)) . n ) ; :: thesis: for x being FinSequence of U1 st x in dom o1 holds
(Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
then A10: o2 = QuotOp (o1,E) by A9, Def9;
let x be FinSequence of U1; :: thesis: ( x in dom o1 implies (Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) )
reconsider x1 = x as Element of the carrier of U1 * by FINSEQ_1:def 11;
reconsider fx = (Nat_Hom (U1,E)) * x as FinSequence of Class E ;
reconsider fx = fx as Element of (Class E) * by FINSEQ_1:def 11;
A11: len ((Nat_Hom (U1,E)) * x) = len x by FINSEQ_3:120;

now :: thesis: for m being Nat st m in dom x holds
Class (E,(x . m)) = fx . m

let m be Nat; :: thesis: ( m in dom x implies Class (E,(x . m)) = fx . m )
assume A12: m in dom x ; :: thesis: Class (E,(x . m)) = fx . m
then A13: m in dom ((Nat_Hom (U1,E)) * x) by FINSEQ_3:120;
x . m in rng x by A12, FUNCT_1:def 3;
then reconsider xm = x . m as Element of the carrier of U1 ;
thus Class (E,(x . m)) = (Nat_Hom (U1,E)) . xm by Def11
.= fx . m by A13, FINSEQ_3:120 ; :: thesis: verum

end;

then A14: x is_representatives_FS fx by A11, FINSEQ_3:def 4;
assume A15: x in dom o1 ; :: thesis: (Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x)
then o1 . x in rng o1 by FUNCT_1:def 3;
then reconsider ox = o1 . x as Element of the carrier of U1 ;
dom o1 = (arity o1) -tuples_on the carrier of U1 by MARGREL1:22
.= { p where p is Element of the carrier of U1 * : len p = arity o1 } by FINSEQ_2:def 4 ;
then A16: ex p being Element of the carrier of U1 * st
( p = x1 & len p = arity o1 ) by A15;
A17: (Nat_Hom (U1,E)) . (o1 . x) = Class (E,ox) by Def11
.= Class (E,(o1 . x)) ;
dom (QuotOp (o1,E)) = (arity o1) -tuples_on (Class E) by Def8
.= { q where q is Element of (Class E) * : len q = arity o1 } by FINSEQ_2:def 4 ;
then fx in dom (QuotOp (o1,E)) by A16, A11;
hence (Nat_Hom (U1,E)) . (o1 . x) = o2 . ((Nat_Hom (U1,E)) * x) by A17, A10, A14, Def8; :: thesis: verum