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 & rng f c= the carrier of T' & rng g c= the carrier' of 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 & rng f c= the carrier of T' & rng g c= the carrier' of 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 & rng f c= the carrier of T' & rng g c= the carrier' of T' holds
f,g form_morphism_between S,T'
let f, g be Function; :: thesis: ( f,g form_morphism_between S,T & rng f c= the carrier of T' & rng g c= the carrier' of T' implies f,g form_morphism_between S,T' )
assume that
A1: ( dom f = the carrier of S & dom g = the carrier' of S ) and
( rng f c= the carrier of T & rng g c= the carrier' of T ) and
A2: f * the ResultSort of S = the ResultSort of T * g and
A3: 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
A4: ( rng f c= the carrier of T' & rng g c= the carrier' of T' ) ; :: according to PUA2MSS1:def 13 :: thesis: f,g form_morphism_between S,T'
thus ( dom f = the carrier of S & dom g = the carrier' of S ) by A1; :: according to PUA2MSS1:def 13 :: thesis: ( rng f c= the carrier of T' & rng g c= the carrier' of T' & the ResultSort of S * f = g * the ResultSort of T' & ( 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 T' . (g . b₁) ) ) )
thus ( rng f c= the carrier of T' & rng g c= the carrier' of T' ) by A4; :: thesis: ( the ResultSort of S * f = g * the ResultSort of T' & ( 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 T' . (g . b₁) ) ) )
thus f * the ResultSort of S = the ResultSort of T * ((id the carrier' of T') * g) by A2, A4, RELAT_1:79
.= (the ResultSort of T * (id the carrier' of T')) * g by RELAT_1:55
.= (the ResultSort of T | the carrier' of T') * g by RELAT_1:94
.= the ResultSort of T' * g by Th13 ; :: 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 T' . (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 T' . (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 T' . (g . o) )
assume A5: ( o in the carrier' of S & p = the Arity of S . o ) ; :: thesis: p * f = the Arity of T' . (g . o)
then g . o in rng g by A1, FUNCT_1:def 5;
then ( g . o in the carrier' of T' & the Arity of T' c= the Arity of T & dom the Arity of T' = the carrier' of T' ) by A4, Th12, FUNCT_2:def 1;
then the Arity of T' . (g . o) = the Arity of T . (g . o) by GRFUNC_1:8;
hence p * f = the Arity of T' . (g . o) by A3, A5; :: thesis: verum