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;
hence MSAlg h is ManySortedSet of {0 } ; :: thesis: verum