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

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