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 that

A1: the carrier of T c= the carrier of S and

A2: the Arity of T c= the Arity of S and

A3: 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 ) ; :: according to PUA2MSS1:def 12,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_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of T or not b_{2} = the Arity of T . b_{1} or b_{2} * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b_{1}) ) ) )

thus rng (id the carrier of T) c= the carrier of S by A1; :: 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_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of T or not b_{2} = the Arity of T . b_{1} or b_{2} * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b_{1}) ) ) )

A4: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;

( dom the Arity of S = the carrier' of S & rng (id the carrier' of T) = the carrier' of T ) by FUNCT_2:def 1;

hence rng (id the carrier' of T) c= the carrier' of S by A2, A4, GRFUNC_1:2; :: thesis: ( the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of T or not b_{2} = the Arity of T . b_{1} or b_{2} * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b_{1}) ) ) )

A5: dom the ResultSort of T = the carrier' of T by Th7;

rng the ResultSort of T c= the carrier of T by RELAT_1:def 19;

hence (id the carrier of T) * the ResultSort of T = the ResultSort of T by RELAT_1:53

.= the ResultSort of S | the carrier' of T by A3, A5, GRFUNC_1:23

.= the ResultSort of S * (id the carrier' of T) by RELAT_1:65 ;

:: thesis: for b_{1} being set

for b_{2} being set holds

( not b_{1} in the carrier' of T or not b_{2} = the Arity of T . b_{1} or b_{2} * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b_{1}) )

let o be set ; :: thesis: for b_{1} being set holds

( not o in the carrier' of T or not b_{1} = the Arity of T . o or b_{1} * (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 that

A6: o in the carrier' of T and

A7: p = the Arity of T . o ; :: thesis: p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o)

reconsider q = p as Element of the carrier of T * by A6, A7, FUNCT_2:5;

rng q c= the carrier of T by FINSEQ_1:def 4;

hence (id the carrier of T) * p = p by RELAT_1:53

.= the Arity of S . o by A2, A4, A6, A7, GRFUNC_1:2

.= the Arity of S . ((id the carrier' of T) . o) by A6, FUNCT_1:17 ;

:: thesis: verum

assume that

A1: the carrier of T c= the carrier of S and

A2: the Arity of T c= the Arity of S and

A3: 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 ) ; :: according to PUA2MSS1:def 12,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

for b

( not b

thus rng (id the carrier of T) c= the carrier of S by A1; :: 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

for b

( not b

A4: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;

( dom the Arity of S = the carrier' of S & rng (id the carrier' of T) = the carrier' of T ) by FUNCT_2:def 1;

hence rng (id the carrier' of T) c= the carrier' of S by A2, A4, GRFUNC_1:2; :: thesis: ( the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b

for b

( not b

A5: dom the ResultSort of T = the carrier' of T by Th7;

rng the ResultSort of T c= the carrier of T by RELAT_1:def 19;

hence (id the carrier of T) * the ResultSort of T = the ResultSort of T by RELAT_1:53

.= the ResultSort of S | the carrier' of T by A3, A5, GRFUNC_1:23

.= the ResultSort of S * (id the carrier' of T) by RELAT_1:65 ;

:: thesis: for b

for b

( not b

let o be set ; :: thesis: for b

( not o in the carrier' of T or not b

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 that

A6: o in the carrier' of T and

A7: p = the Arity of T . o ; :: thesis: p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o)

reconsider q = p as Element of the carrier of T * by A6, A7, FUNCT_2:5;

rng q c= the carrier of T by FINSEQ_1:def 4;

hence (id the carrier of T) * p = p by RELAT_1:53

.= the Arity of S . o by A2, A4, A6, A7, GRFUNC_1:2

.= the Arity of S . ((id the carrier' of T) . o) by A6, FUNCT_1:17 ;

:: thesis: verum