let UA1, UA2 be Universal_Algebra; :: thesis: ( UA1,UA2 are_similar implies for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2 )
reconsider f = (*--> 0 ) * (signature UA1) as Function of (dom (signature UA1)),({0 } * ) by MSUALG_1:7;
A1: 0 in {0 } by TARSKI:def 1;
assume UA1,UA2 are_similar ; :: thesis: for F being ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)) holds F . 0 is Function of UA1,UA2
then MSSign UA1 = MSSign UA2 by MSUHOM_1:10;
then A2: ( MSAlg UA2 = MSAlgebra(# (MSSorts UA2),(MSCharact UA2) #) & (MSAlg UA2) Over (MSSign UA1) = MSAlg UA2 ) by MSUALG_1:def 16, MSUHOM_1:9;
let F be ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)); :: thesis: F . 0 is Function of UA1,UA2
A3: ( the carrier of (MSSign UA1) = {0 } & MSAlg UA1 = MSAlgebra(# (MSSorts UA1),(MSCharact UA1) #) ) by MSUALG_1:def 13, MSUALG_1:def 16;
A4: (MSSorts UA2) . 0 = (0 .--> the carrier of UA2) . 0 by MSUALG_1:def 14
.= the carrier of UA2 by A1, FUNCOP_1:13 ;
(MSSorts UA1) . 0 = (0 .--> the carrier of UA1) . 0 by MSUALG_1:def 14
.= the carrier of UA1 by A1, FUNCOP_1:13 ;
hence F . 0 is Function of UA1,UA2 by A1, A3, A4, A2, PBOOLE:def 18; :: thesis: verum