the carrier of (MSSign U2) = {0} by MSUALG_1:def 8;
then reconsider Z2 = the Sorts of (MSAlg U2) as ManySortedSet of {0} ;
set f = 0 .--> h;
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 11;
then A2: the Sorts of (MSAlg U2) . 0 = (0 .--> the carrier of U2) . 0 by MSUALG_1:def 9
.= the carrier of U2 by FUNCOP_1:72 ;
A3: the carrier of (MSSign U1) = {0} by MSUALG_1:def 8;
then reconsider Z1 = the Sorts of (MSAlg U1) as ManySortedSet of {0} ;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 11;
then A4: the Sorts of (MSAlg U1) . 0 = (0 .--> the carrier of U1) . 0 by MSUALG_1:def 9
.= the carrier of U1 by FUNCOP_1:72 ;
now :: thesis: for a being object st a in {0} holds
(0 .--> h) . a is Function of ( the Sorts of (MSAlg U1) . a),( the Sorts of (MSAlg U2) . a)
let a be object ; :: 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, A2, FUNCOP_1:72; :: thesis: verum
end;
then 0 .--> h is ManySortedFunction of Z1,Z2 by PBOOLE:def 15;
hence 0 .--> h is ManySortedFunction of (MSAlg U1),((MSAlg U2) Over (MSSign U1)) by A1, A3, Th9; :: thesis: verum