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

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