let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st U1,U2 are_similar holds
MSAlg h is ManySortedSet of {0 }
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar implies MSAlg h is ManySortedSet of {0 } )
assume U1,U2 are_similar ; :: thesis: MSAlg h is ManySortedSet of {0 }
then MSAlg h = 0 .--> h by Def3, Th10;
then dom (MSAlg h) = {0 } by FUNCOP_1:19;
hence MSAlg h is ManySortedSet of {0 } by PBOOLE:def 3; :: thesis: verum