let S be feasible ManySortedSign ; :: thesis: for S' 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 S',g | the carrier' of S' form_morphism_between S',T
let S' 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 S',g | the carrier' of S' form_morphism_between S',T
A1: id the carrier of S', id the carrier' of S' form_morphism_between S',S by Def2;
let T be ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S',g | the carrier' of S' form_morphism_between S',T
let f, g be Function; :: thesis: ( f,g form_morphism_between S,T implies f | the carrier of S',g | the carrier' of S' form_morphism_between S',T )
( f | the carrier of S' = f * (id the carrier of S') & g | the carrier' of S' = g * (id the carrier' of S') ) by RELAT_1:94;
hence ( f,g form_morphism_between S,T implies f | the carrier of S',g | the carrier' of S' form_morphism_between S',T ) by A1, PUA2MSS1:30; :: thesis: verum