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
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar implies MSAlg h is ManySortedSet of )
assume U1,U2 are_similar ; :: thesis: MSAlg h is ManySortedSet of
then MSAlg h = 0 .--> h by Def3, Th10;
then dom (MSAlg h) = {0 } by FUNCOP_1:19;
hence MSAlg h is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum