let S be ManySortedSign ; :: thesis: for T being feasible ManySortedSign
for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
let T be feasible ManySortedSign ; :: thesis: for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
let T9 be Subsignature of T; :: thesis: for f, g being Function st f,g form_morphism_between S,T9 holds
f,g form_morphism_between S,T
let f, g be Function; :: thesis: ( f,g form_morphism_between S,T9 implies f,g form_morphism_between S,T )
assume A1: f,g form_morphism_between S,T9 ; :: thesis: f,g form_morphism_between S,T
rng f c= the carrier of T9 by A1;
then A2: (id the carrier of T9) * f = f by RELAT_1:53;
rng g c= the carrier' of T9 by A1;
then A3: (id the carrier' of T9) * g = g by RELAT_1:53;
id the carrier of T9, id the carrier' of T9 form_morphism_between T9,T by Def2;
hence f,g form_morphism_between S,T by A1, A2, A3, PUA2MSS1:29; :: thesis: verum