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;

.= 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

( 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

the ResultSort of T =
(id the carrier of T) * the ResultSort of T
by FUNCT_2:17
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;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

.= 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