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 b_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of S or not b_{2} = the Arity of S . b_{1} or b_{2} * f = the Arity of T9 . (g . b_{1}) ) ) )

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 b_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of S or not b_{2} = the Arity of S . b_{1} or b_{2} * f = the Arity of T9 . (g . b_{1}) ) ) )

thus f * the ResultSort of S = the ResultSort of T * ((id the carrier' of T9) * g) by A3, A6, RELAT_1:53

.= ( 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 b_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of S or not b_{2} = the Arity of S . b_{1} or b_{2} * f = the Arity of T9 . (g . b_{1}) )

let o be set ; :: thesis: for b_{1} being set holds

( not o in the carrier' of S or not b_{1} = the Arity of S . o or b_{1} * 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 Th11, FUNCT_2:def 1;

g . o in rng g by A2, A7, FUNCT_1:def 3;

then the Arity of T9 . (g . o) = the Arity of T . (g . o) by A6, A9, GRFUNC_1:2;

hence p * f = the Arity of T9 . (g . o) by A4, A7, A8; :: thesis: verum

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 b

for b

( not b

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 b

for b

( not b

thus f * the ResultSort of S = the ResultSort of T * ((id the carrier' of T9) * g) by A3, A6, RELAT_1:53

.= ( 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 b

for b

( not b

let o be set ; :: thesis: for b

( not o in the carrier' of S or not b

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 Th11, FUNCT_2:def 1;

g . o in rng g by A2, A7, FUNCT_1:def 3;

then the Arity of T9 . (g . o) = the Arity of T . (g . o) by A6, A9, GRFUNC_1:2;

hence p * f = the Arity of T9 . (g . o) by A4, A7, A8; :: thesis: verum