let U1, U2, U3 be Universal_Algebra; for h1 being Function of U1,U2
for h2 being Function of U2,U3 st h1 is_homomorphism & h2 is_homomorphism holds
h2 * h1 is_homomorphism
let h1 be Function of U1,U2; for h2 being Function of U2,U3 st h1 is_homomorphism & h2 is_homomorphism holds
h2 * h1 is_homomorphism
let h2 be Function of U2,U3; ( h1 is_homomorphism & h2 is_homomorphism implies h2 * h1 is_homomorphism )
set s1 = signature U1;
set s2 = signature U2;
set s3 = signature U3;
assume that
A1:
h1 is_homomorphism
and
A2:
h2 is_homomorphism
; h2 * h1 is_homomorphism
U1,U2 are_similar
by A1;
then A3:
signature U1 = signature U2
;
U2,U3 are_similar
by A2;
hence
signature U1 = signature U3
by A3; UNIALG_2:def 1,ALG_1:def 1 for n being Nat st n in dom the charact of U1 holds
for o1 being operation of U1
for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x)
let n be Nat; ( n in dom the charact of U1 implies for o1 being operation of U1
for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x) )
assume A4:
n in dom the charact of U1
; for o1 being operation of U1
for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x)
let o1 be operation of U1; for o2 being operation of U3 st o1 = the charact of U1 . n & o2 = the charact of U3 . n holds
for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o2 . ((h2 * h1) * x)
let o3 be operation of U3; ( o1 = the charact of U1 . n & o3 = the charact of U3 . n implies for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o3 . ((h2 * h1) * x) )
assume that
A5:
o1 = the charact of U1 . n
and
A6:
o3 = the charact of U3 . n
; for x being FinSequence of U1 st x in dom o1 holds
(h2 * h1) . (o1 . x) = o3 . ((h2 * h1) * x)
let a be FinSequence of U1; ( a in dom o1 implies (h2 * h1) . (o1 . a) = o3 . ((h2 * h1) * a) )
reconsider b = h1 * a as Element of the carrier of U2 * by FINSEQ_1:def 11;
assume A7:
a in dom o1
; (h2 * h1) . (o1 . a) = o3 . ((h2 * h1) * a)
then A8:
o1 . a in rng o1
by FUNCT_1:def 3;
dom o1 = (arity o1) -tuples_on the carrier of U1
by MARGREL1:22;
then
a in { w where w is Element of the carrier of U1 * : len w = arity o1 }
by A7, FINSEQ_2:def 4;
then A9:
ex w being Element of the carrier of U1 * st
( w = a & len w = arity o1 )
;
A10:
( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) )
by FINSEQ_1:def 3, UNIALG_1:def 4;
A11:
( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) )
by FINSEQ_1:def 3, UNIALG_1:def 4;
then reconsider o2 = the charact of U2 . n as operation of U2 by A3, A10, A4, FUNCT_1:def 3;
A12:
dom (signature U1) = Seg (len (signature U1))
by FINSEQ_1:def 3;
then A13:
(signature U2) . n = arity o2
by A3, A10, A4, UNIALG_1:def 4;
(signature U1) . n = arity o1
by A10, A12, A4, A5, UNIALG_1:def 4;
then
len (h1 * a) = arity o2
by A3, A13, A9, FINSEQ_3:120;
then
( dom o2 = (arity o2) -tuples_on the carrier of U2 & b in { s where s is Element of the carrier of U2 * : len s = arity o2 } )
by MARGREL1:22;
then
h1 * a in dom o2
by FINSEQ_2:def 4;
then A14:
h2 . (o2 . (h1 * a)) = o3 . (h2 * (h1 * a))
by A2, A3, A10, A11, A4, A6;
h1 . (o1 . a) = o2 . (h1 * a)
by A1, A4, A5, A7;
hence (h2 * h1) . (o1 . a) =
o3 . (h2 * (h1 * a))
by A8, A14, FUNCT_2:15
.=
o3 . ((h2 * h1) * a)
by Th4
;
verum