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₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S or not b₂ = the Arity of S . b₁ or b₂ * f = the Arity of T9 . (g . 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₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S or not b₂ = the Arity of S . b₁ or b₂ * f = the Arity of T9 . (g . 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₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S or not b₂ = the Arity of S . b₁ or b₂ * f = the Arity of T9 . (g . b₁) )
let o be set ; :: thesis: for b₁ being set holds
( not o in the carrier' of S or not b₁ = the Arity of S . o or b₁ * 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