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 )
assume A1: 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
let F be ManySortedFunction of (MSAlg UA1),((MSAlg UA2) Over (MSSign UA1)); :: thesis: F . 0 is Function of UA1,UA2
A2: MSSign UA1 = MSSign UA2 by A1, MSUHOM_1:10;
reconsider f = (*--> 0 ) * (signature UA1) as Function of (dom (signature UA1)),({0 } * ) by MSUALG_1:7;
A3: ( the carrier of (MSSign UA1) = {0 } & the carrier' of (MSSign UA1) = dom (signature UA1) & the Arity of (MSSign UA1) = f & the ResultSort of (MSSign UA1) = (dom (signature UA1)) --> 0 ) by MSUALG_1:def 13;
A4: 0 in {0 } by TARSKI:def 1;
A5: (MSSorts UA1) . 0 = (0 .--> the carrier of UA1) . 0 by MSUALG_1:def 14
.= the carrier of UA1 by A4, FUNCOP_1:13 ;
A6: MSAlg UA1 = MSAlgebra(# (MSSorts UA1),(MSCharact UA1) #) by MSUALG_1:def 16;
A7: (MSSorts UA2) . 0 = (0 .--> the carrier of UA2) . 0 by MSUALG_1:def 14
.= the carrier of UA2 by A4, FUNCOP_1:13 ;
A8: MSAlg UA2 = MSAlgebra(# (MSSorts UA2),(MSCharact UA2) #) by MSUALG_1:def 16;
(MSAlg UA2) Over (MSSign UA1) = MSAlg UA2 by A2, MSUHOM_1:9;
hence F . 0 is Function of UA1,UA2 by A3, A4, A5, A6, A7, A8, PBOOLE:def 18; :: thesis: verum