let U1 be Universal_Algebra; :: thesis: for E being Congruence of U1 holds Nat_Hom U1,E is_homomorphism U1, QuotUnivAlg U1,E
let E be Congruence of U1; :: thesis: Nat_Hom U1,E is_homomorphism U1, QuotUnivAlg U1,E
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 11;
A2: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def 3;
A3: len (QuotOpSeq U1,E) = len the charact of U1 by Def13;
A4: len (signature (QuotUnivAlg U1,E)) = len the charact of (QuotUnivAlg U1,E) by UNIALG_1:def 11;

now

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 5;
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 Def13;
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 set 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 Def12;
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 26;
( n in dom (signature (QuotUnivAlg U1,E)) & (signature U1) . n = arity o1 ) by A3, A4, A1, A2, A5, FINSEQ_1:def 3, UNIALG_1:def 11;
hence (signature U1) . n = (signature (QuotUnivAlg U1,E)) . n by A6, A8, UNIALG_1:def 11; :: thesis: verum

end;

hence signature U1 = signature (QuotUnivAlg U1,E) by A3, A4, A1, FINSEQ_2:10; :: according to UNIALG_2:def 2,ALG_1:def 1 :: thesis: for n being Element of 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 Element of 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, Def13;
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:129;

now

let m be Element of 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:129;
x . m in rng x by A12, FUNCT_1:def 5;
then reconsider xm = x . m as Element of the carrier of U1 ;
thus Class E,(x . m) = (Nat_Hom U1,E) . xm by Def15
.= fx . m by A13, FINSEQ_3:129 ; :: 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 5;
then reconsider ox = o1 . x as Element of the carrier of U1 ;
dom o1 = (arity o1) -tuples_on the carrier of U1 by MARGREL1:58
.= { 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 Def15
.= Class E,(o1 . x) ;
dom (QuotOp o1,E) = (arity o1) -tuples_on (Class E) by Def12
.= { 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, Def12; :: thesis: verum