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,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9

let T be feasible ManySortedSign ; :: thesis: for T9 being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9

let T9 be Subsignature of T; :: thesis: for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds
f,g form_morphism_between S,T9

let f, g be Function; :: thesis: ( f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 implies f,g form_morphism_between S,T9 )
assume that
A1: dom f = the carrier of S and
A2: dom g = the carrier' of S and
rng f c= the carrier of T and
rng g c= the carrier' of T and
A3: f * the ResultSort of S = the ResultSort of T * g and
A4: for o being set
for p being Function st o in the carrier' of S & p = the Arity of S . o holds
f * p = the Arity of T . (g . o) and
A5: rng f c= the carrier of T9 and
A6: rng g c= the carrier' of T9 ; :: according to PUA2MSS1:def 12 :: thesis: f,g form_morphism_between S,T9
thus ( dom f = the carrier of S & dom g = the carrier' of S ) by A1, A2; :: according to PUA2MSS1:def 12 :: thesis: ( rng f c= the carrier of T9 & rng g c= the carrier' of T9 & the ResultSort of S * f = g * the ResultSort of T9 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) ) )

thus ( rng f c= the carrier of T9 & rng g c= the carrier' of T9 ) by A5, A6; :: thesis: ( the ResultSort of S * f = g * the ResultSort of T9 & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) ) )

thus f * the ResultSort of S = the ResultSort of T * ((id the carrier' of T9) * g) by
.= ( the ResultSort of T * (id the carrier' of T9)) * g by RELAT_1:36
.= ( the ResultSort of T | the carrier' of T9) * g by RELAT_1:65
.= the ResultSort of T9 * g by Th12 ; :: thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) )

let o be set ; :: thesis: for b1 being set holds
( not o in the carrier' of S or not b1 = the Arity of S . o or b1 * f = the Arity of T9 . (g . o) )

let p be Function; :: thesis: ( not o in the carrier' of S or not p = the Arity of S . o or p * f = the Arity of T9 . (g . o) )
assume that
A7: o in the carrier' of S and
A8: p = the Arity of S . o ; :: thesis: p * f = the Arity of T9 . (g . o)
A9: ( the Arity of T9 c= the Arity of T & dom the Arity of T9 = the carrier' of T9 ) by ;
g . o in rng g by ;
then the Arity of T9 . (g . o) = the Arity of T . (g . o) by ;
hence p * f = the Arity of T9 . (g . o) by A4, A7, A8; :: thesis: verum