let S be feasible ManySortedSign ; :: thesis: for T being Subsignature of S holds
( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
let T be Subsignature of S; :: thesis: ( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
set f = id the carrier of T;
set g = id the carrier' of T;
A1: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;
A2: id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;
A3: now :: thesis: for x being object st x in dom the Arity of T holds
the Arity of T . x = the Arity of S . x
let x be object ; :: thesis: ( x in dom the Arity of T implies the Arity of T . x = the Arity of S . x )
A4: rng the Arity of T c= the carrier of T * by RELAT_1:def 19;
assume A5: x in dom the Arity of T ; :: thesis: the Arity of T . x = the Arity of S . x
then the Arity of T . x in rng the Arity of T by FUNCT_1:def 3;
then reconsider p = the Arity of T . x as Element of the carrier of T * by A4;
(id the carrier' of T) . x = x by A1, A5, FUNCT_1:17;
then ( rng p c= the carrier of T & (id the carrier of T) * p = the Arity of S . x ) by A2, A1, A5, FINSEQ_1:def 4;
hence the Arity of T . x = the Arity of S . x by RELAT_1:53; :: thesis: verum
end;
the ResultSort of T = (id the carrier of T) * the ResultSort of T by FUNCT_2:17
.= the ResultSort of S * (id the carrier' of T) by A2 ;
hence the ResultSort of T c= the ResultSort of S by RELAT_1:50; :: thesis: the Arity of T c= the Arity of S
dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then dom the Arity of T c= dom the Arity of S by A1, Th10;
hence the Arity of T c= the Arity of S by A3, GRFUNC_1:2; :: thesis: verum