theorem Th1: :: MSUHOM_1:1
theorem Th2: :: MSUHOM_1:2
theorem :: MSUHOM_1:3
theorem Th4: :: MSUHOM_1:4
:: deftheorem Def1 defines <= MSUHOM_1:def 1 :
theorem :: MSUHOM_1:5
theorem :: MSUHOM_1:6
theorem :: MSUHOM_1:7
theorem Th8: :: MSUHOM_1:8
:: deftheorem Def2 defines Over MSUHOM_1:def 2 :
theorem Th9: :: MSUHOM_1:9
theorem Th10: :: MSUHOM_1:10
:: deftheorem Def3 defines MSAlg MSUHOM_1:def 3 :
theorem Th11: :: MSUHOM_1:11
theorem Th12: :: MSUHOM_1:12
Lm1:
for U1 being Universal_Algebra holds dom (signature U1) = dom the charact of U1
theorem Th13: :: MSUHOM_1:13
Lm2:
for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for o being OperSymbol of (MSSign U1) holds Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2
theorem Th14: :: MSUHOM_1:14
theorem Th15: :: MSUHOM_1:15
theorem Th16: :: MSUHOM_1:16
Lm3:
for U1 being Universal_Algebra
for n being Nat st n in dom the charact of U1 holds
n is OperSymbol of (MSSign U1)
theorem Th17: :: MSUHOM_1:17
theorem Th18: :: MSUHOM_1:18
theorem Th19: :: MSUHOM_1:19
theorem :: MSUHOM_1:20
theorem Th21: :: MSUHOM_1:21
theorem Th22: :: MSUHOM_1:22
theorem Th23: :: MSUHOM_1:23
theorem :: MSUHOM_1:24
theorem :: MSUHOM_1:25
theorem :: MSUHOM_1:26