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
rng f c= the carrier of T' by A1, PUA2MSS1:def 13;
then A2: (id the carrier of T') * f = f by RELAT_1:79;
rng g c= the carrier' of T' by A1, PUA2MSS1:def 13;
then A3: (id the carrier' of T') * g = g by RELAT_1:79;
id the carrier of T', id the carrier' of T' form_morphism_between T',T by Def2;
hence f,g form_morphism_between S,T by A1, A2, A3, PUA2MSS1:30; :: thesis: verum