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