let U1, U2, U3 be Universal_Algebra; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1: ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U2,U3 ) ; :: thesis: h2 * h1 is_homomorphism U1,U3
then ( U1,U2 are_similar & U2,U3 are_similar ) by Def1;
then A2: ( signature U1 = signature U2 & signature U2 = signature U3 ) by UNIALG_2:def 2;
hence signature U1 = signature U3 ; :: 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 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)
A3: ( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def 11;
A4: ( dom the charact of U1 = Seg (len the charact of U1) & dom the charact of U2 = Seg (len the charact of U2) & dom (signature U1) = Seg (len (signature U1)) & dom (signature U2) = Seg (len (signature U2)) ) by FINSEQ_1:def 3;
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 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 A5: n in dom the charact of U1 ; :: thesis: 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)
then reconsider o2 = the charact of U2 . n as operation of U2 by A2, A3, A4, FUNCT_1:def 5;
let o1 be operation of U1; :: thesis: 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; :: thesis: ( 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 A6: ( o1 = the charact of U1 . n & o3 = the charact of U3 . n ) ; :: thesis: 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; :: thesis: ( a in dom o1 implies (h2 * h1) . (o1 . a) = o3 . ((h2 * h1) * a) )
assume A7: a in dom o1 ; :: thesis: (h2 * h1) . (o1 . a) = o3 . ((h2 * h1) * a)
then A8: ( o1 . a in rng o1 & rng o1 c= the carrier of U1 ) by FUNCT_1:def 5;
A9: ( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A2, A3, A4, A5, A6, UNIALG_1:def 11;
A10: ( dom o2 = (arity o2) -tuples_on the carrier of U2 & 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 consider w being Element of the carrier of U1 * such that
A11: ( w = a & len w = arity o1 ) ;
reconsider b = h1 * a as Element of the carrier of U2 * by FINSEQ_1:def 11;
len (h1 * a) = arity o2 by A2, A9, A11, Th1;
then b in { s where s is Element of the carrier of U2 * : len s = arity o2 } ;
then h1 * a in dom o2 by A10, FINSEQ_2:def 4;
then ( h1 . (o1 . a) = o2 . (h1 * a) & h2 . (o2 . (h1 * a)) = o3 . (h2 * (h1 * a)) ) by A1, A2, A3, A4, A5, A6, A7, Def1;
hence (h2 * h1) . (o1 . a) = o3 . (h2 * (h1 * a)) by A8, FUNCT_2:21
.= o3 . ((h2 * h1) * a) by Th5 ;
:: thesis: verum