let S1, S2 be non void Signature; 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; 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; ( 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
; (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;
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; verum