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