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 )
assume A1: f,g form_morphism_between S1,S2 ; :: thesis: (f * ) * the Arity of S1 = the Arity of S2 * g
then A2: ( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by PUA2MSS1:def 13;
A3: ( dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the carrier' of S2 ) by FUNCT_2:def 1;
then A4: dom (the Arity of S2 * g) = the carrier' of S1 by A2, RELAT_1:46;
A5: dom ((f * ) * the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

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 A6: c in the carrier' of S1 ; :: thesis: ((f * ) * the Arity of S1) . c = (the Arity of S2 * g) . c
then A7: the Arity of S1 . c in rng the Arity of S1 by A3, 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 A3, A6, FUNCT_1:23
.= f * p by A7, LANG1:def 14
.= the Arity of S2 . (g . c) by A1, A6, PUA2MSS1:def 13
.= (the Arity of S2 * g) . c by A2, A6, FUNCT_1:23 ; :: thesis: verum

end;

hence (f * ) * the Arity of S1 = the Arity of S2 * g by A4, A5, FUNCT_1:9; :: thesis: verum