let S1 be non empty feasible ManySortedSign ; :: thesis: for S2 being non empty Subsignature of S1
for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
let S2 be non empty Subsignature of S1; :: thesis: for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
let S3 be non empty Subsignature of S2; :: thesis: for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3
let A be MSAlgebra over S1; :: thesis: A | S3 = (A | S2) | S3
set f1 = id the carrier of S2;
set g1 = id the carrier' of S2;
set f2 = id the carrier of S3;
set g2 = id the carrier' of S3;
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 S2, id the carrier' of S2 form_morphism_between S2,S1 & id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S2 ) by Def2;
hence A | S3 = (A | S2) | S3 by A1, A2, Th27; :: thesis: verum