let S be feasible ManySortedSign ; for S9 being Subsignature of S
for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
let S9 be Subsignature of S; for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
let T be ManySortedSign ; for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T
let f, g be Function; ( f,g form_morphism_between S,T implies f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T )
A1:
g | the carrier' of S9 = g * (id the carrier' of S9)
by RELAT_1:65;
( id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S & f | the carrier of S9 = f * (id the carrier of S9) )
by Def2, RELAT_1:65;
hence
( f,g form_morphism_between S,T implies f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T )
by A1, PUA2MSS1:29; verum