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 )
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 11, 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 8, MSUALG_1:def 11;
A4: (MSSorts UA2) . 0 = (0 .--> the carrier of UA2) . 0 by MSUALG_1:def 9
.= the carrier of UA2 by A1, FUNCOP_1:7 ;
(MSSorts UA1) . 0 = (0 .--> the carrier of UA1) . 0 by MSUALG_1:def 9
.= the carrier of UA1 by A1, FUNCOP_1:7 ;
hence F . 0 is Function of UA1,UA2 by A1, A3, A4, A2, PBOOLE:def 15; :: thesis: verum