let S be ManySortedSign ; 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 ; 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; 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; ( 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
; PUA2MSS1:def 12 f,g form_morphism_between S,T9
thus
( dom f = the carrier of S & dom g = the carrier' of S )
by A1, A2; PUA2MSS1:def 12 ( 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; ( 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 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
; 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 ; 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; ( 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
; 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; verum