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 ;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;

A6: now :: thesis: for c being object st c in the carrier' of S1 holds
((f *) * the Arity of S1) . c = ( the Arity of S2 * g) . c

let c be object ; :: 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 3;
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:13
.= f * p by A8, LANG1:def 13
.= the Arity of S2 . (g . c) by A3, A7
.= ( the Arity of S2 * g) . c by A4, A7, FUNCT_1:13 ; :: thesis: verum

end;

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