let S1, S2, S3 be ManySortedSign ; for f1, f2, g1, g2 being Function st f1,g1 form_morphism_between S1,S2 & f2,g2 form_morphism_between S2,S3 holds
f2 * f1,g2 * g1 form_morphism_between S1,S3
let f1, f2, g1, g2 be Function; ( f1,g1 form_morphism_between S1,S2 & f2,g2 form_morphism_between S2,S3 implies f2 * f1,g2 * g1 form_morphism_between S1,S3 )
assume that
A1:
dom f1 = the carrier of S1
and
A2:
dom g1 = the carrier' of S1
and
A3:
rng f1 c= the carrier of S2
and
A4:
rng g1 c= the carrier' of S2
and
A5:
f1 * the ResultSort of S1 = the ResultSort of S2 * g1
and
A6:
for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f1 * p = the Arity of S2 . (g1 . o)
and
A7:
dom f2 = the carrier of S2
and
A8:
dom g2 = the carrier' of S2
and
A9:
rng f2 c= the carrier of S3
and
A10:
rng g2 c= the carrier' of S3
and
A11:
f2 * the ResultSort of S2 = the ResultSort of S3 * g2
and
A12:
for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f2 * p = the Arity of S3 . (g2 . o)
; PUA2MSS1:def 12 f2 * f1,g2 * g1 form_morphism_between S1,S3
set f = f2 * f1;
set g = g2 * g1;
thus
( dom (f2 * f1) = the carrier of S1 & dom (g2 * g1) = the carrier' of S1 )
by A1, A2, A3, A4, A7, A8, RELAT_1:27; PUA2MSS1:def 12 ( rng (f2 * f1) c= the carrier of S3 & rng (g2 * g1) c= the carrier' of S3 & (f2 * f1) * the ResultSort of S1 = the ResultSort of S3 * (g2 * g1) & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) ) )
A13:
rng (f2 * f1) c= rng f2
by RELAT_1:26;
rng (g2 * g1) c= rng g2
by RELAT_1:26;
hence
( rng (f2 * f1) c= the carrier of S3 & rng (g2 * g1) c= the carrier' of S3 )
by A9, A10, A13; ( (f2 * f1) * the ResultSort of S1 = the ResultSort of S3 * (g2 * g1) & ( for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) ) )
thus (f2 * f1) * the ResultSort of S1 =
f2 * ( the ResultSort of S2 * g1)
by A5, RELAT_1:36
.=
(f2 * the ResultSort of S2) * g1
by RELAT_1:36
.=
the ResultSort of S3 * (g2 * g1)
by A11, RELAT_1:36
; for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
let o be set ; for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
let p be Function; ( o in the carrier' of S1 & p = the Arity of S1 . o implies (f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o) )
assume that
A14:
o in the carrier' of S1
and
A15:
p = the Arity of S1 . o
; (f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
A16:
f1 * p = the Arity of S2 . (g1 . o)
by A6, A14, A15;
A17:
g1 . o in rng g1
by A2, A14, FUNCT_1:def 3;
A18:
(f2 * f1) * p = f2 * (f1 * p)
by RELAT_1:36;
(g2 * g1) . o = g2 . (g1 . o)
by A2, A14, FUNCT_1:13;
hence
(f2 * f1) * p = the Arity of S3 . ((g2 * g1) . o)
by A4, A12, A16, A17, A18; verum