set f = 0 .--> h;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 16;
then A4: the Sorts of (MSAlg U1) . 0 = (0 .--> the carrier of U1) . 0 by MSUALG_1:def 14
.= the carrier of U1 by FUNCOP_1:87 ;
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 16;
then A5: the Sorts of (MSAlg U2) . 0 = (0 .--> the carrier of U2) . 0 by MSUALG_1:def 14
.= the carrier of U2 by FUNCOP_1:87 ;

A6: now

let a be set ; :: thesis: ( a in {0 } implies (0 .--> h) . a is Function of (the Sorts of (MSAlg U1) . a),(the Sorts of (MSAlg U2) . a) )
assume a in {0 } ; :: thesis: (0 .--> h) . a is Function of (the Sorts of (MSAlg U1) . a),(the Sorts of (MSAlg U2) . a)
then a = 0 by TARSKI:def 1;
hence (0 .--> h) . a is Function of (the Sorts of (MSAlg U1) . a),(the Sorts of (MSAlg U2) . a) by A4, A5, FUNCOP_1:87; :: thesis: verum

end;

reconsider g = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A7: ( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = g & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def 13;
then reconsider Z1 = the Sorts of (MSAlg U1) as ManySortedSet of ;
the carrier of (MSSign U2) = {0 } by MSUALG_1:def 13;
then reconsider Z2 = the Sorts of (MSAlg U2) as ManySortedSet of ;
0 .--> h is ManySortedFunction of Z1,Z2 by A6, PBOOLE:def 18;
hence 0 .--> h is ManySortedFunction of (MSAlg U1),((MSAlg U2) Over (MSSign U1)) by A1, A7, Th9; :: thesis: verum