let S1 be feasible ManySortedSign ; :: thesis: for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1
let S2 be Subsignature of S1; :: thesis: for S3 being Subsignature of S2 holds S3 is Subsignature of S1
let S3 be Subsignature of S2; :: thesis: S3 is Subsignature of S1
rng (id the carrier of S3) = the carrier of S3 ;
then A1: (id the carrier of S2) * (id the carrier of S3) = id the carrier of S3 by Th10, RELAT_1:53;
rng (id the carrier' of S3) = the carrier' of S3 ;
then A2: (id the carrier' of S2) * (id the carrier' of S3) = id the carrier' of S3 by Th10, RELAT_1:53;
( id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S2 & id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 ) by Def2;
hence id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S1 by A1, A2, PUA2MSS1:29; :: according to INSTALG1:def 2 :: thesis: verum