let S1, S2 be non void Signature; :: thesis: for f being Function of the carrier of S1,the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
(f * ) * the Arity of S1 = the Arity of S2 * g
let f be Function of the carrier of S1,the carrier of S2; :: thesis: for g being Function st f,g form_morphism_between S1,S2 holds
(f * ) * the Arity of S1 = the Arity of S2 * g
let g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies (f * ) * the Arity of S1 = the Arity of S2 * g )
A1: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
A2: dom ((f * ) * the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;
assume A3: f,g form_morphism_between S1,S2 ; :: thesis: (f * ) * the Arity of S1 = the Arity of S2 * g
then A4: dom g = the carrier' of S1 by PUA2MSS1:def 13;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;

A6: now

let c be set ; :: thesis: ( c in the carrier' of S1 implies ((f * ) * the Arity of S1) . c = (the Arity of S2 * g) . c )
assume A7: c in the carrier' of S1 ; :: thesis: ((f * ) * the Arity of S1) . c = (the Arity of S2 * g) . c
then A8: the Arity of S1 . c in rng the Arity of S1 by A5, FUNCT_1:def 5;
then reconsider p = the Arity of S1 . c as FinSequence of the carrier of S1 by FINSEQ_1:def 11;
thus ((f * ) * the Arity of S1) . c = (f * ) . p by A5, A7, FUNCT_1:23
.= f * p by A8, LANG1:def 14
.= the Arity of S2 . (g . c) by A3, A7, PUA2MSS1:def 13
.= (the Arity of S2 * g) . c by A4, A7, FUNCT_1:23 ; :: thesis: verum

end;

rng g c= the carrier' of S2 by A3, PUA2MSS1:def 13;
then dom (the Arity of S2 * g) = the carrier' of S1 by A4, A1, RELAT_1:46;
hence (f * ) * the Arity of S1 = the Arity of S2 * g by A2, A6, FUNCT_1:9; :: thesis: verum