:: MSUALG_9 semantic presentation

scheme :: MSUALG_9:sch 1
s1{ F₁() -> non empty set , P₁[ set , set ] } :

ex b₁ being ManySortedSet of F₁() st
for b₂ being Element of F₁() holds P₁[b₂,b₁ . b₂]

provided

E1: for b₁ being Element of F₁() ex b₂ being set st P₁[b₁,b₂]

proof end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster locally-finite Element of Bool a₂;
existence

proof end;

end;

registration

let c₁ be set ;
let c₂ be V2 ManySortedSet of c₁;
cluster V2 locally-finite ManySortedSubset of a₂;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be OperSymbol of c₁;
cluster -> FinSequence-like Element of Args a₃,a₂;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be set ;
let c₃ be SortSymbol of c₁;
let c₄ be MSAlgebra-Family of c₂,c₁;
cluster -> Relation-like Function-like Element of (SORTS a₄) . a₃;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
cluster FreeGen a₂ -> V2 free ;
coherence by MSAFREE:15, MSAFREE:17;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V2 ManySortedSet of the carrier of c₁;
cluster FreeMSA a₂ -> free ;
coherence by MSAFREE:18;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂, c₃ be non-empty MSAlgebra of c₁;
cluster [:a₂,a₃:] -> non-empty ;
coherence

proof end;

end;

theorem Th1: :: MSUALG_9:1

for b₁, b₂, b₃ being set
for b₄ being Function st b₁ in dom b₄ & b₄ . b₁ in [:b₂,b₃:] holds
b₄ . b₁ = [((pr1 b₄) . b₁),((pr2 b₄) . b₁)]

proof end;

theorem Th2: :: MSUALG_9:2

for b₁ being non empty set
for b₂ being set
for b₃ being Function of b₁,{b₂} holds rng b₃ = {b₂}

proof end;

theorem Th3: :: MSUALG_9:3

for b₁ being non empty finite set ex b₂ being Function of NAT ,b₁ st rng b₂ = b₁

proof end;

theorem Th4: :: MSUALG_9:4

for b₁ being set holds Class (nabla b₁) c= {b₁}

proof end;

theorem Th5: :: MSUALG_9:5

for b₁ being non empty set holds Class (nabla b₁) = {b₁}

proof end;

theorem Th6: :: MSUALG_9:6

for b₁, b₂ being set ex b₃ being ManySortedSet of b₁ st {b₃} = b₁ --> {b₂}

proof end;

theorem Th7: :: MSUALG_9:7

for b₁ being set
for b₂ being ManySortedSet of b₁ ex b₃ being V2 ManySortedSet of b₁ st b₂ c= b₃

proof end;

theorem Th8: :: MSUALG_9:8

for b₁ being set
for b₂ being V2 ManySortedSet of b₁
for b₃ being locally-finite ManySortedSubset of b₂ ex b₄ being V2 locally-finite ManySortedSubset of b₂ st b₃ c= b₄

proof end;

theorem Th9: :: MSUALG_9:9

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄, b₅ being ManySortedFunction of b₂,{b₃} holds b₄ = b₅

proof end;

theorem Th10: :: MSUALG_9:10

for b₁ being set
for b₂ being V2 ManySortedSet of b₁
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,{b₃} holds b₄ is "onto"

proof end;

theorem Th11: :: MSUALG_9:11

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being V2 ManySortedSet of b₁
for b₄ being ManySortedFunction of {b₂},b₃ holds b₄ is "1-1"

proof end;

theorem Th12: :: MSUALG_9:12

for b₁ being non empty non void ManySortedSign
for b₂ being V2 ManySortedSet of the carrier of b₁ holds Reverse b₂ is "1-1"

proof end;

theorem Th13: :: MSUALG_9:13

for b₁ being set
for b₂ being V2 locally-finite ManySortedSet of b₁ ex b₃ being ManySortedFunction of b₁ --> NAT ,b₂ st b₃ is "onto"

proof end;

theorem Th14: :: MSUALG_9:14

for b₁ being non empty ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being Element of product the Sorts of b₂ st ( for b₅ being set holds (proj the Sorts of b₂,b₅) . b₃ = (proj the Sorts of b₂,b₅) . b₄ ) holds
b₃ = b₄

proof end;

theorem Th15: :: MSUALG_9:15

for b₁ being non empty non void ManySortedSign
for b₂ being non empty set
for b₃ being Element of b₁
for b₄ being MSAlgebra-Family of b₂,b₁
for b₅, b₆ being Element of product (Carrier b₄,b₃) st ( for b₇ being Element of b₂ holds (proj (Carrier b₄,b₃),b₇) . b₅ = (proj (Carrier b₄,b₃),b₇) . b₆ ) holds
b₅ = b₆

proof end;

theorem Th16: :: MSUALG_9:16

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being non-empty MSSubAlgebra of b₂
for b₅ being ManySortedFunction of b₃,b₄ st b₅ is_homomorphism b₃,b₄ holds
for b₆ being ManySortedFunction of b₃,b₂ st b₅ = b₆ holds
b₆ is_homomorphism b₃,b₂

proof end;

theorem Th17: :: MSUALG_9:17

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_monomorphism b₂,b₃ holds
b₂, Image b₄ are_isomorphic

proof end;

theorem Th18: :: MSUALG_9:18

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is "onto" holds
for b₅ being OperSymbol of b₁
for b₆ being Element of Args b₅,b₃ ex b₇ being Element of Args b₅,b₂ st b₄ # b₇ = b₆

proof end;

theorem Th19: :: MSUALG_9:19

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄ being Element of Args b₃,b₂ holds (Den b₃,b₂) . b₄ in the Sorts of b₂ . (the_result_sort_of b₃)

proof end;

theorem Th20: :: MSUALG_9:20

for b₁ being non empty non void ManySortedSign
for b₂, b₃, b₄ being non-empty MSAlgebra of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₂,b₄ st b₅ is_epimorphism b₂,b₃ & b₆ is_homomorphism b₂,b₄ holds
for b₇ being ManySortedFunction of b₃,b₄ st b₇ ** b₅ = b₆ holds
b₇ is_homomorphism b₃,b₄

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be V2 ManySortedSet of c₁;
let c₅ be ManySortedFunction of c₂,[|c₃,c₄|];
func Mpr1 c₅ -> ManySortedFunction of a₂,a₃ means :Def1: :: MSUALG_9:def 1
for b₁ being set st b₁ in a₁ holds
a₆ . b₁ = pr1 (a₅ . b₁);
existence

proof end;

uniqueness

proof end;

func Mpr2 c₅ -> ManySortedFunction of a₂,a₄ means :Def2: :: MSUALG_9:def 2
for b₁ being set st b₁ in a₁ holds
a₆ . b₁ = pr2 (a₅ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Mpr1 MSUALG_9:def 1 :

:: deftheorem Def2 defines Mpr2 MSUALG_9:def 2 :

theorem Th21: :: MSUALG_9:21

for b₁, b₂ being set
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₃,[|(b₁ --> {b₂}),(b₁ --> {b₂})|] holds Mpr1 b₄ = Mpr2 b₄

proof end;

theorem Th22: :: MSUALG_9:22

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,[|b₃,b₄|] st b₅ is "onto" holds
Mpr1 b₅ is "onto"

proof end;

theorem Th23: :: MSUALG_9:23

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,[|b₃,b₄|] st b₅ is "onto" holds
Mpr2 b₅ is "onto"

proof end;

theorem Th24: :: MSUALG_9:24

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄, b₅ being V2 ManySortedSet of b₁
for b₆ being ManySortedFunction of b₂,[|b₄,b₅|] st b₃ in doms b₆ holds
for b₇ being set st b₇ in b₁ holds
(b₆ .. b₃) . b₇ = [(((Mpr1 b₆) .. b₃) . b₇),(((Mpr2 b₆) .. b₃) . b₇)]

proof end;

registration

let c₁ be non empty ManySortedSign ;
cluster the Sorts of (Trivial_Algebra a₁) -> V2 locally-finite ;
coherence

proof end;

end;

registration

let c₁ be non empty ManySortedSign ;
cluster Trivial_Algebra a₁ -> non-empty locally-finite ;
coherence

proof end;

end;

theorem Th25: :: MSUALG_9:25

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedFunction of b₂,(Trivial_Algebra b₁)
for b₄ being OperSymbol of b₁
for b₅ being Element of Args b₄,b₂ holds
( (b₃ . (the_result_sort_of b₄)) . ((Den b₄,b₂) . b₅) = 0 & (Den b₄,(Trivial_Algebra b₁)) . (b₃ # b₅) = 0 )

proof end;

theorem Th26: :: MSUALG_9:26

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being ManySortedFunction of b₂,(Trivial_Algebra b₁) holds b₃ is_epimorphism b₂, Trivial_Algebra b₁

proof end;

theorem Th27: :: MSUALG_9:27

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ st ex b₃ being ManySortedSet of the carrier of b₁ st the Sorts of b₂ = {b₃} holds
b₂, Trivial_Algebra b₁ are_isomorphic

proof end;

theorem Th28: :: MSUALG_9:28

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSCongruence of b₂ holds b₃ is ManySortedSubset of [|the Sorts of b₂,the Sorts of b₂|]

proof end;

theorem Th29: :: MSUALG_9:29

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Subset of (CongrLatt b₂)
for b₄ being SubsetFamily of [|the Sorts of b₂,the Sorts of b₂|] st b₃ = b₄ holds
meet |:b₄:| is MSCongruence of b₂

proof end;

theorem Th30: :: MSUALG_9:30

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSCongruence of b₂ st b₃ = [|the Sorts of b₂,the Sorts of b₂|] holds
the Sorts of (QuotMSAlg b₂,b₃) = {the Sorts of b₂}

proof end;

theorem Th31: :: MSUALG_9:31

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ holds
(MSHomQuot b₄) ** (MSNat_Hom b₂,(MSCng b₄)) = b₄

proof end;

theorem Th32: :: MSUALG_9:32

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSCongruence of b₂
for b₄ being SortSymbol of b₁
for b₅ being Element of the Sorts of (QuotMSAlg b₂,b₃) . b₄ ex b₆ being Element of the Sorts of b₂ . b₄ st b₅ = Class b₃,b₆

proof end;

theorem Th33: :: MSUALG_9:33

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃, b₄ being MSEquivalence-like ManySortedRelation of b₂ st b₃ c= b₄ holds
for b₅ being Element of b₁
for b₆, b₇ being Element of the Sorts of b₂ . b₅ st [b₆,b₇] in b₃ . b₅ holds
( Class b₃,b₆ c= Class b₄,b₇ & ( b₂ is non-empty implies Class b₃,b₇ c= Class b₄,b₆ ) )

proof end;

theorem Th34: :: MSUALG_9:34

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSCongruence of b₂
for b₄ being SortSymbol of b₁
for b₅, b₆ being Element of the Sorts of b₂ . b₄ holds
( ((MSNat_Hom b₂,b₃) . b₄) . b₅ = ((MSNat_Hom b₂,b₃) . b₄) . b₆ iff [b₅,b₆] in b₃ . b₄ )

proof end;

E17: now

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃, c₄ be MSCongruence of c₂;
let c₅ be ManySortedFunction of (QuotMSAlg c₂,c₃),(QuotMSAlg c₂,c₄);
assume E18: for b₁ being Element of c₁
for b₂ being Element of the Sorts of (QuotMSAlg c₂,c₃) . b₁
for b₃ being Element of the Sorts of c₂ . b₁ st b₂ = Class c₃,b₃ holds
(c₅ . b₁) . b₂ = Class c₄,b₃ ;
thus c₅ is "onto"

proof

set c₆ = the Sorts of (QuotMSAlg c₂,c₃);
set c₇ = the Sorts of (QuotMSAlg c₂,c₄);
let c₈ be set ; :: according to MSUALG_3:def 3
assume c₈ in the carrier of c₁ ;
then reconsider c₉ = c₈ as SortSymbol of c₁ ;
rng (c₅ . c₉) c= the Sorts of (QuotMSAlg c₂,c₄) . c₉ by RELSET_1:12;
hence rng (c₅ . c₈) c= the Sorts of (QuotMSAlg c₂,c₄) . c₈ ; :: according to XBOOLE_0:def 10
let c₁₀ be set ; :: according to TARSKI:def 3
assume E19: c₁₀ in the Sorts of (QuotMSAlg c₂,c₄) . c₈ ;
c₁₀ in Class (c₄ . c₉) by E19, MSUALG_4:def 8;
then consider c₁₁ being set such that
E20: c₁₁ in the Sorts of c₂ . c₉ and
E21: c₁₀ = Class (c₄ . c₉),c₁₁ by EQREL_1:def 5;
reconsider c₁₂ = c₁₁ as Element of the Sorts of c₂ . c₉ by E20;
E22: dom (c₅ . c₉) = the Sorts of (QuotMSAlg c₂,c₃) . c₉ by FUNCT_2:def 1;
Class (c₃ . c₉),c₁₂ in Class (c₃ . c₉) by EQREL_1:def 5;
then Class c₃,c₁₂ in Class (c₃ . c₉) ;
then reconsider c₁₃ = Class c₃,c₁₂ as Element of the Sorts of (QuotMSAlg c₂,c₃) . c₉ by MSUALG_4:def 8;
(c₅ . c₉) . c₁₃ = Class c₄,c₁₂ by E18
.= Class (c₄ . c₉),c₁₂ ;
hence c₁₀ in rng (c₅ . c₈) by E21, E22, FUNCT_1:def 5;

end;

theorem Th35: :: MSUALG_9:35

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being MSCongruence of b₂
for b₅ being ManySortedFunction of (QuotMSAlg b₂,b₃),(QuotMSAlg b₂,b₄) st ( for b₆ being Element of b₁
for b₇ being Element of the Sorts of (QuotMSAlg b₂,b₃) . b₆
for b₈ being Element of the Sorts of b₂ . b₆ st b₇ = Class b₃,b₈ holds
(b₅ . b₆) . b₇ = Class b₄,b₈ ) holds
b₅ ** (MSNat_Hom b₂,b₃) = MSNat_Hom b₂,b₄

proof end;

theorem Th36: :: MSUALG_9:36

proof end;

theorem Th37: :: MSUALG_9:37

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is_homomorphism b₂,b₃ holds
for b₅ being MSCongruence of b₂ st b₅ c= MSCng b₄ holds
ex b₆ being ManySortedFunction of (QuotMSAlg b₂,b₅),b₃ st
( b₆ is_homomorphism QuotMSAlg b₂,b₅,b₃ & b₄ = b₆ ** (MSNat_Hom b₂,b₅) )

proof end;