let S1 be non empty ManySortedSign ; :: thesis: for S2 being non empty Subsignature of S1

for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

let S2 be non empty Subsignature of S1; :: thesis: for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

set f = id the carrier of S2;

set g = id the carrier' of S2;

let A be MSAlgebra over S1; :: thesis: (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2;

then (id the Sorts of A) * (id the carrier of S2) = id the Sorts of (A | S2) by Th31;

hence (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) by RELAT_1:65; :: thesis: verum

for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

let S2 be non empty Subsignature of S1; :: thesis: for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

set f = id the carrier of S2;

set g = id the carrier' of S2;

let A be MSAlgebra over S1; :: thesis: (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2;

then (id the Sorts of A) * (id the carrier of S2) = id the Sorts of (A | S2) by Th31;

hence (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) by RELAT_1:65; :: thesis: verum