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 & rng (id the carrier' of S3) = the carrier' of S3 & the carrier' of S3 c= the carrier' of S2 & the carrier of S3 c= the carrier of S2 ) by Th11, RELAT_1:71;
then ( (id the carrier of S2) * (id the carrier of S3) = id the carrier of S3 & (id the carrier' of S2) * (id the carrier' of S3) = id the carrier' of S3 & 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, RELAT_1:79;
hence id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S1 by PUA2MSS1:30; :: according to INSTALG1:def 2 :: thesis: verum