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: ( the charact of (QuotUnivAlg U1,E) = QuotOpSeq U1,E & len (QuotOpSeq U1,E) = len the charact of U1 & len (signature (QuotUnivAlg U1,E)) = len the charact of (QuotUnivAlg U1,E) & len (signature U1) = len the charact of U1 ) by Def13, UNIALG_1:def 11;
X: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def 3;

now

let n be Nat; :: thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature (QuotUnivAlg U1,E)) . n )
assume Z: n in dom (signature U1) ; :: thesis: (signature U1) . n = (signature (QuotUnivAlg U1,E)) . n
then A2: ( n in dom (signature U1) & n in dom the charact of U1 & n in dom (QuotOpSeq U1,E) & n in dom (signature (QuotUnivAlg U1,E)) ) by A1, FINSEQ_1:def 3, X;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def 5;
A3: (signature U1) . n = arity o1 by Z, UNIALG_1:def 11;
A4: (QuotOpSeq U1,E) . n = QuotOp o1,E by A2, Def13;
A5: dom (QuotOp o1,E) = (arity o1) -tuples_on (Class E) by Def12;
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
A6: b in dom cl by XBOOLE_0:def 1;
reconsider b = b as Element of the carrier of (QuotUnivAlg U1,E) * by A6;
b in { w where w is Element of (Class E) * : len w = arity o1 } by A5, A6, FINSEQ_2:def 4;
then consider w being Element of (Class E) * such that
A7: ( w = b & len w = arity o1 ) ;
arity cl = arity o1 by A6, A7, UNIALG_1:def 10;
hence (signature U1) . n = (signature (QuotUnivAlg U1,E)) . n by A2, A3, A4, UNIALG_1:def 11; :: thesis: verum

end;

hence signature U1 = signature (QuotUnivAlg U1,E) by 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 A8: n in dom (QuotOpSeq U1,E) by A1, 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 A9: ( 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)
let x be FinSequence of U1; :: thesis: ( x in dom o1 implies (Nat_Hom U1,E) . (o1 . x) = o2 . ((Nat_Hom U1,E) * x) )
assume A10: x in dom o1 ; :: thesis: (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;
dom o1 = (arity o1) -tuples_on the carrier of U1 by UNIALG_2:2
.= { p where p is Element of the carrier of U1 * : len p = arity o1 } by FINSEQ_2:def 4 ;
then A11: ex p being Element of the carrier of U1 * st
( p = x1 & len p = arity o1 ) by A10;
( rng o1 c= the carrier of U1 & o1 . x in rng o1 ) by A10, FUNCT_1:def 5;
then reconsider ox = o1 . x as Element of the carrier of U1 ;
A12: (Nat_Hom U1,E) . (o1 . x) = Class E,ox by Def15
.= Class E,(o1 . x) ;
A13: o2 = QuotOp o1,E by A8, A9, Def13;
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;
A14: 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 ;
A15: len ((Nat_Hom U1,E) * x) = len x by Th1;
then A16: fx in dom (QuotOp o1,E) by A11, A14;

now

let m be Element of NAT ; :: thesis: ( m in dom x implies Class E,(x . m) = fx . m )
assume A17: m in dom x ; :: thesis: Class E,(x . m) = fx . m
then A18: m in dom ((Nat_Hom U1,E) * x) by Th1;
( x . m in rng x & rng x c= the carrier of U1 ) by A17, 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 A18, Th1 ; :: thesis: verum

end;

then x is_representatives_FS fx by A15, Def11;
hence (Nat_Hom U1,E) . (o1 . x) = o2 . ((Nat_Hom U1,E) * x) by A12, A13, A16, Def12; :: thesis: verum