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

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