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 U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3
let h1 be Function of U1,U2; for h2 being Function of U2,U3 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 holds
h2 * h1 is_homomorphism U1,U3
let h2 be Function of U2,U3; ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 implies h2 * h1 is_homomorphism U1,U3 )
set s1 = signature U1;
set s2 = signature U2;
set s3 = signature U3;
assume that
A1:
h1 is_homomorphism U1,U2
and
A2:
h2 is_homomorphism U2,U3
; h2 * h1 is_homomorphism U1,U3
U1,U2 are_similar
by A1, Def1;
then A3:
signature U1 = signature U2
by UNIALG_2:def 2;
U2,U3 are_similar
by A2, Def1;
hence
signature U1 = signature U3
by A3, UNIALG_2:def 2; UNIALG_2:def 2,ALG_1:def 1 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 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 Element of 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 5;
dom o1 = (arity o1) -tuples_on the carrier of U1
by UNIALG_2:2;
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 11;
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 11;
then reconsider o2 = the charact of U2 . n as operation of U2 by A3, A10, A4, FUNCT_1:def 5;
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 11;
(signature U1) . n = arity o1
by A10, A12, A4, A5, UNIALG_1:def 11;
then
len (h1 * a) = arity o2
by A3, A13, A9, Th1;
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 UNIALG_2:2;
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, Def1;
h1 . (o1 . a) = o2 . (h1 * a)
by A1, A4, A5, A7, Def1;
hence (h2 * h1) . (o1 . a) =
o3 . (h2 * (h1 * a))
by A8, A14, FUNCT_2:21
.=
o3 . ((h2 * h1) * a)
by Th5
;
verum