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