let S be feasible ManySortedSign ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: verum