:: MSUHOM_1 semantic presentation

theorem Th1: :: MSUHOM_1:1

for b₁, b₂ being Function
for b₃ being set st rng b₁ c= b₃ holds
(b₂ | b₃) * b₁ = b₂ * b₁

proof end;

theorem Th2: :: MSUHOM_1:2

for b₁ being set
for b₂ being Subset of b₁ holds b₂ * c= b₁ *

proof end;

theorem Th3: :: MSUHOM_1:3

for b₁ being Function
for b₂ being set st b₁ is Function-yielding holds
b₁ | b₂ is Function-yielding

proof end;

theorem Th4: :: MSUHOM_1:4

for b₁ being set
for b₂ being Subset of b₁
for b₃ being ManySortedSet of b₁ holds (b₃ | b₂) # = (b₃ # ) | (b₂ * )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be Element of c₁;
redefine func |-> as c₂ |-> c₃ -> FinSequence of a₁;
coherence by FINSEQ_2:77;

end;

definition

let c₁, c₂ be non empty ManySortedSign ;
pred c₁ <= c₂ means :Def1: :: MSUHOM_1:def 1
( the carrier of a₁ c= the carrier of a₂ & the OperSymbols of a₁ c= the OperSymbols of a₂ & the Arity of a₂ | the OperSymbols of a₁ = the Arity of a₁ & the ResultSort of a₂ | the OperSymbols of a₁ = the ResultSort of a₁ );
reflexivity

proof end;

end;

:: deftheorem Def1 defines <= MSUHOM_1:def 1 :

theorem Th5: :: MSUHOM_1:5

for b₁, b₂, b₃ being non empty ManySortedSign st b₁ <= b₂ & b₂ <= b₃ holds
b₁ <= b₃

proof end;

theorem Th6: :: MSUHOM_1:6

for b₁, b₂ being non empty strict ManySortedSign st b₁ <= b₂ & b₂ <= b₁ holds
b₁ = b₂

proof end;

theorem Th7: :: MSUHOM_1:7

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function
for b₄ being Element of b₂
for b₅ being Nat st 1 <= b₅ & b₅ <= b₁ holds
(b₄ .--> b₃) . ((b₁ |-> b₄) /. b₅) = b₃

proof end;

theorem Th8: :: MSUHOM_1:8

for b₁ being set
for b₂ being Subset of b₁
for b₃, b₄ being ManySortedSet of b₁
for b₅ being ManySortedFunction of b₃,b₄
for b₆, b₇ being ManySortedSet of b₂ st b₆ = b₃ | b₂ & b₇ = b₄ | b₂ holds
b₅ | b₂ is ManySortedFunction of b₆,b₇

proof end;

definition

let c₁, c₂ be non empty strict non void ManySortedSign ;
let c₃ be strict non-empty MSAlgebra of c₂;
assume E6: c₁ <= c₂ ;
func c₃ Over c₁ -> strict non-empty MSAlgebra of a₁ means :Def2: :: MSUHOM_1:def 2
( the Sorts of a₄ = the Sorts of a₃ | the carrier of a₁ & the Charact of a₄ = the Charact of a₃ | the OperSymbols of a₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines Over MSUHOM_1:def 2 :

theorem Th9: :: MSUHOM_1:9

for b₁ being non empty strict non void ManySortedSign
for b₂ being strict non-empty MSAlgebra of b₁ holds b₂ = b₂ Over b₁

proof end;

theorem Th10: :: MSUHOM_1:10

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
MSSign b₁ = MSSign b₂

proof end;

definition

let c₁, c₂ be Universal_Algebra;
let c₃ be Function of c₁,c₂;
assume E9: MSSign c₁ = MSSign c₂ ;
func MSAlg c₃ -> ManySortedFunction of (MSAlg a₁),((MSAlg a₂) Over (MSSign a₁)) equals :Def3: :: MSUHOM_1:def 3
{0} --> a₃;
coherence

proof end;

end;

:: deftheorem Def3 defines MSAlg MSUHOM_1:def 3 :

theorem Th11: :: MSUHOM_1:11

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar holds
for b₄ being OperSymbol of (MSSign b₁) holds (MSAlg b₃) . (the_result_sort_of b₄) = b₃

proof end;

theorem Th12: :: MSUHOM_1:12

for b₁ being Universal_Algebra
for b₂ being OperSymbol of (MSSign b₁) holds Den b₂,(MSAlg b₁) = the charact of b₁ . b₂

proof end;

Lemma12: for b₁ being Universal_Algebra holds dom (signature b₁) = dom the charact of b₁

proof end;

theorem Th13: :: MSUHOM_1:13

for b₁ being Universal_Algebra
for b₂ being OperSymbol of (MSSign b₁) holds Den b₂,(MSAlg b₁) is operation of b₁

proof end;

Lemma14: for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
for b₃ being OperSymbol of (MSSign b₁) holds Den b₃,((MSAlg b₂) Over (MSSign b₁)) is operation of b₂

proof end;

theorem Th14: :: MSUHOM_1:14

for b₁ being Universal_Algebra
for b₂ being OperSymbol of (MSSign b₁)
for b₃ being Element of Args b₂,(MSAlg b₁) holds b₃ is FinSequence of the carrier of b₁

proof end;

theorem Th15: :: MSUHOM_1:15

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar holds
for b₄ being OperSymbol of (MSSign b₁)
for b₅ being Element of Args b₄,(MSAlg b₁) holds (MSAlg b₃) # b₅ = b₃ * b₅

proof end;

theorem Th16: :: MSUHOM_1:16

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_homomorphism b₁,b₂ holds
MSAlg b₃ is_homomorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁)

proof end;

Lemma18: for b₁ being Universal_Algebra
for b₂ being Nat st b₂ in dom the charact of b₁ holds
b₂ is OperSymbol of (MSSign b₁)

proof end;

theorem Th17: :: MSUHOM_1:17

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar holds
MSAlg b₃ is ManySortedSet of {0}

proof end;

theorem Th18: :: MSUHOM_1:18

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_epimorphism b₁,b₂ holds
MSAlg b₃ is_epimorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁)

proof end;

theorem Th19: :: MSUHOM_1:19

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_monomorphism b₁,b₂ holds
MSAlg b₃ is_monomorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁)

proof end;

theorem Th20: :: MSUHOM_1:20

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₃ is_isomorphism b₁,b₂ holds
MSAlg b₃ is_isomorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁)

proof end;

theorem Th21: :: MSUHOM_1:21

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar & MSAlg b₃ is_homomorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁) holds
b₃ is_homomorphism b₁,b₂

proof end;

theorem Th22: :: MSUHOM_1:22

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar & MSAlg b₃ is_epimorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁) holds
b₃ is_epimorphism b₁,b₂

proof end;

theorem Th23: :: MSUHOM_1:23

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar & MSAlg b₃ is_monomorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁) holds
b₃ is_monomorphism b₁,b₂

proof end;

theorem Th24: :: MSUHOM_1:24

for b₁, b₂ being Universal_Algebra
for b₃ being Function of b₁,b₂ st b₁,b₂ are_similar & MSAlg b₃ is_isomorphism MSAlg b₁,(MSAlg b₂) Over (MSSign b₁) holds
b₃ is_isomorphism b₁,b₂

proof end;

theorem Th25: :: MSUHOM_1:25

for b₁ being Universal_Algebra holds MSAlg (id the carrier of b₁) = id the Sorts of (MSAlg b₁)

proof end;

theorem Th26: :: MSUHOM_1:26

for b₁, b₂, b₃ being Universal_Algebra st b₁,b₂ are_similar & b₂,b₃ are_similar holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ holds (MSAlg b₅) ** (MSAlg b₄) = MSAlg (b₅ * b₄)

proof end;