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

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