let S1 be non empty ManySortedSign ; :: thesis: for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra of 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 of 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 of 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 Th10;
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, Th30;
hence h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2),the Sorts of (A2 | S2) by RELAT_1:94; :: thesis: verum