let S1, S2, S3 be ManySortedSign ; :: thesis: 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; :: thesis: ( 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) ; :: according to PUA2MSS1:def 12 :: thesis: 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; :: according to PUA2MSS1:def 12 :: thesis: ( 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; :: thesis: ( (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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum