let S1 be non empty ManySortedSign ; :: thesis: for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
let S2 be non empty Subsignature of S1; :: thesis: for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
set f = id the carrier of S2;
set g = id the carrier' of S2;
let A1, A2 be MSAlgebra over S1; :: thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; :: thesis: h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)
A1: id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2;
then reconsider f = id the carrier of S2 as Function of the carrier of S2, the carrier of S1 by Th9;
h * f is ManySortedFunction of the Sorts of (A1 | (S2,f,(id the carrier' of S2))), the Sorts of (A2 | (S2,f,(id the carrier' of S2))) by A1, Th29;
hence h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) by RELAT_1:65; :: thesis: verum