let S, T be feasible ManySortedSign ; :: thesis: ( the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S implies T is Subsignature of S )
assume A1: ( the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S ) ; :: thesis: T is Subsignature of S
set f = id the carrier of T;
set g = id the carrier' of T;
thus ( dom (id the carrier of T) = the carrier of T & dom (id the carrier' of T) = the carrier' of T ) by RELAT_1:71; :: according to PUA2MSS1:def 13,INSTALG1:def 2 :: thesis: ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S & the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of T or not b₂ = the Arity of T . b₁ or b₂ * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b₁) ) ) )
thus rng (id the carrier of T) c= the carrier of S by A1, RELAT_1:71; :: thesis: ( rng (id the carrier' of T) c= the carrier' of S & the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of T or not b₂ = the Arity of T . b₁ or b₂ * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b₁) ) ) )
A2: ( dom the Arity of T = the carrier' of T & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1;
A3: ( dom the ResultSort of T = the carrier' of T & dom the ResultSort of S = the carrier' of S ) by Th8;
A4: ( rng the ResultSort of T c= the carrier of T & rng the ResultSort of S c= the carrier of S ) by RELSET_1:12;
rng (id the carrier' of T) = the carrier' of T by RELAT_1:71;
hence rng (id the carrier' of T) c= the carrier' of S by A1, A2, GRFUNC_1:8; :: thesis: ( the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of T or not b₂ = the Arity of T . b₁ or b₂ * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b₁) ) ) )
thus (id the carrier of T) * the ResultSort of T = the ResultSort of T by A4, RELAT_1:79
.= the ResultSort of S | the carrier' of T by A1, A3, GRFUNC_1:64
.= the ResultSort of S * (id the carrier' of T) by RELAT_1:94 ; :: thesis: for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of T or not b₂ = the Arity of T . b₁ or b₂ * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b₁) )
let o be set ; :: thesis: for b₁ being set holds
( not o in the carrier' of T or not b₁ = the Arity of T . o or b₁ * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) )
let p be Function; :: thesis: ( not o in the carrier' of T or not p = the Arity of T . o or p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) )
assume A5: ( o in the carrier' of T & p = the Arity of T . o ) ; :: thesis: p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o)
then reconsider q = p as Element of the carrier of T * by FUNCT_2:7;
rng q c= the carrier of T by FINSEQ_1:def 4;
hence (id the carrier of T) * p = p by RELAT_1:79
.= the Arity of S . o by A1, A2, A5, GRFUNC_1:8
.= the Arity of S . ((id the carrier' of T) . o) by A5, FUNCT_1:34 ;
:: thesis: verum