:: by Adam Grabowski

::

:: Received June 11, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

registration

let I be non empty set ;

let S be non empty non void ManySortedSign ;

let AF be MSAlgebra-Family of I,S;

let i be Element of I;

let o be OperSymbol of S;

coherence

( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like )

end;
let S be non empty non void ManySortedSign ;

let AF be MSAlgebra-Family of I,S;

let i be Element of I;

let o be OperSymbol of S;

coherence

( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like )

proof end;

registration

let I be non empty set ;

let S be non empty non void ManySortedSign ;

let AF be MSAlgebra-Family of I,S;

let s be SortSymbol of S;

coherence

(SORTS AF) . s is functional

end;
let S be non empty non void ManySortedSign ;

let AF be MSAlgebra-Family of I,S;

let s be SortSymbol of S;

coherence

(SORTS AF) . s is functional

proof end;

definition

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

ex b_{1} being MSAlgebra-Family of the carrier of P,S ex F being ManySortedFunction of the InternalRel of P st

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (b_{1} . i),(b_{1} . j) ex f2 being ManySortedFunction of (b_{1} . j),(b_{1} . k) st

( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b_{1} . i,b_{1} . j )

end;
let S be non empty non void ManySortedSign ;

mode OrderedAlgFam of P,S -> MSAlgebra-Family of the carrier of P,S means :Def1: :: MSALIMIT:def 1

ex F being ManySortedFunction of the InternalRel of P st

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (it . i),(it . j) ex f2 being ManySortedFunction of (it . j),(it . k) st

( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism it . i,it . j );

existence ex F being ManySortedFunction of the InternalRel of P st

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (it . i),(it . j) ex f2 being ManySortedFunction of (it . j),(it . k) st

( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism it . i,it . j );

ex b

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (b

( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b

proof end;

:: deftheorem Def1 defines OrderedAlgFam MSALIMIT:def 1 :

for P being non empty Poset

for S being non empty non void ManySortedSign

for b_{3} being MSAlgebra-Family of the carrier of P,S holds

( b_{3} is OrderedAlgFam of P,S iff ex F being ManySortedFunction of the InternalRel of P st

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (b_{3} . i),(b_{3} . j) ex f2 being ManySortedFunction of (b_{3} . j),(b_{3} . k) st

( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b_{3} . i,b_{3} . j ) );

for P being non empty Poset

for S being non empty non void ManySortedSign

for b

( b

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (b

( f1 = F . (j,i) & f2 = F . (k,j) & F . (k,i) = f2 ** f1 & f1 is_homomorphism b

definition

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

ex b_{1} being ManySortedFunction of the InternalRel of P st

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st

( f1 = b_{1} . (j,i) & f2 = b_{1} . (k,j) & b_{1} . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j )
by Def1;

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

mode Binding of OAF -> ManySortedFunction of the InternalRel of P means :Def2: :: MSALIMIT:def 2

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st

( f1 = it . (j,i) & f2 = it . (k,j) & it . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j );

existence for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st

( f1 = it . (j,i) & f2 = it . (k,j) & it . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j );

ex b

for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st

( f1 = b

:: deftheorem Def2 defines Binding MSALIMIT:def 2 :

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for b_{4} being ManySortedFunction of the InternalRel of P holds

( b_{4} is Binding of OAF iff for i, j, k being Element of P st i >= j & j >= k holds

ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st

( f1 = b_{4} . (j,i) & f2 = b_{4} . (k,j) & b_{4} . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) );

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for b

( b

ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st

( f1 = b

definition

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

let i, j be Element of P;

assume A1: i >= j ;

B . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

let i, j be Element of P;

assume A1: i >= j ;

func bind (B,i,j) -> ManySortedFunction of (OAF . i),(OAF . j) equals :Def3: :: MSALIMIT:def 3

B . (j,i);

coherence B . (j,i);

B . (j,i) is ManySortedFunction of (OAF . i),(OAF . j)

proof end;

:: deftheorem Def3 defines bind MSALIMIT:def 3 :

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

bind (B,i,j) = B . (j,i);

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

bind (B,i,j) = B . (j,i);

theorem Th1: :: MSALIMIT:1

for P being non empty Poset

for i, j, k being Element of P

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF st i >= j & j >= k holds

(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)

for i, j, k being Element of P

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF st i >= j & j >= k holds

(bind (B,j,k)) ** (bind (B,i,j)) = bind (B,i,k)

proof end;

definition

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let IT be Binding of OAF;

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let IT be Binding of OAF;

attr IT is normalized means :Def4: :: MSALIMIT:def 4

for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i);

for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i);

:: deftheorem Def4 defines normalized MSALIMIT:def 4 :

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for IT being Binding of OAF holds

( IT is normalized iff for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i) );

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for IT being Binding of OAF holds

( IT is normalized iff for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i) );

theorem Th2: :: MSALIMIT:2

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

proof end;

definition

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

ex b_{1} being Binding of OAF st

for i, j being Element of P st i >= j holds

b_{1} . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))))

for b_{1}, b_{2} being Binding of OAF st ( for i, j being Element of P st i >= j holds

b_{1} . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) & ( for i, j being Element of P st i >= j holds

b_{2} . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) holds

b_{1} = b_{2}

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

func Normalized B -> Binding of OAF means :Def5: :: MSALIMIT:def 5

for i, j being Element of P st i >= j holds

it . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))));

existence for i, j being Element of P st i >= j holds

it . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i))));

ex b

for i, j being Element of P st i >= j holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines Normalized MSALIMIT:def 5 :

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B, b_{5} being Binding of OAF holds

( b_{5} = Normalized B iff for i, j being Element of P st i >= j holds

b_{5} . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) );

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B, b

( b

b

theorem Th3: :: MSALIMIT:3

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j & i <> j holds

B . (j,i) = (Normalized B) . (j,i)

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j & i <> j holds

B . (j,i) = (Normalized B) . (j,i)

proof end;

registration

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

coherence

Normalized B is normalized

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

coherence

Normalized B is normalized

proof end;

registration

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

ex b_{1} being Binding of OAF st b_{1} is normalized

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

cluster Relation-like the InternalRel of P -defined Function-like total Function-yielding V45() normalized for Binding of OAF;

existence ex b

proof end;

theorem :: MSALIMIT:4

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for NB being normalized Binding of OAF

for i, j being Element of P st i >= j holds

(Normalized NB) . (j,i) = NB . (j,i)

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for NB being normalized Binding of OAF

for i, j being Element of P st i >= j holds

(Normalized NB) . (j,i) = NB . (j,i)

proof end;

definition

let P be non empty Poset;

let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

ex b_{1} being strict MSSubAlgebra of product OAF st

for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b_{1} . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j )

for b_{1}, b_{2} being strict MSSubAlgebra of product OAF st ( for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b_{1} . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j ) ) & ( for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b_{2} . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j ) ) holds

b_{1} = b_{2}

end;
let S be non empty non void ManySortedSign ;

let OAF be OrderedAlgFam of P,S;

let B be Binding of OAF;

func InvLim B -> strict MSSubAlgebra of product OAF means :Def6: :: MSALIMIT:def 6

for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of it . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j );

existence for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of it . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j );

ex b

for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b

((bind (B,i,j)) . s) . (f . i) = f . j )

proof end;

uniqueness for b

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b

((bind (B,i,j)) . s) . (f . i) = f . j ) ) & ( for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b

((bind (B,i,j)) . s) . (f . i) = f . j ) ) holds

b

proof end;

:: deftheorem Def6 defines InvLim MSALIMIT:def 6 :

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for b_{5} being strict MSSubAlgebra of product OAF holds

( b_{5} = InvLim B iff for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b_{5} . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j ) );

for P being non empty Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for b

( b

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b

((bind (B,i,j)) . s) . (f . i) = f . j ) );

theorem :: MSALIMIT:5

for DP being non empty discrete Poset

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of DP,S

for B being normalized Binding of OAF holds InvLim B = product OAF

for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of DP,S

for B being normalized Binding of OAF holds InvLim B = product OAF

proof end;

definition

let X be set ;

end;
attr X is MSS-membered means :Def7: :: MSALIMIT:def 7

for x being set st x in X holds

x is non empty non void strict ManySortedSign ;

for x being set st x in X holds

x is non empty non void strict ManySortedSign ;

:: deftheorem Def7 defines MSS-membered MSALIMIT:def 7 :

for X being set holds

( X is MSS-membered iff for x being set st x in X holds

x is non empty non void strict ManySortedSign );

for X being set holds

( X is MSS-membered iff for x being set st x in X holds

x is non empty non void strict ManySortedSign );

registration
end;

registration

existence

ex b_{1} being ManySortedSign st

( b_{1} is strict & b_{1} is empty & b_{1} is void )

end;
ex b

( b

proof end;

Lm1: for S being empty void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S

proof end;

Lm2: for S being non empty void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S

proof end;

theorem :: MSALIMIT:6

for S being void ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S

proof end;

definition

let A be non empty set ;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) & ( for x being object holds

( x in b_{2} iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) holds

b_{1} = b_{2}

end;
func MSS_set A -> set means :Def8: :: MSALIMIT:def 9

for x being object holds

( x in it iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) );

existence for x being object holds

( x in it iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) );

ex b

for x being object holds

( x in b

( x = S & the carrier of S c= A & the carrier' of S c= A ) )

proof end;

uniqueness for b

( x in b

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) & ( for x being object holds

( x in b

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) holds

b

proof end;

:: deftheorem Def8 defines MSS_set MSALIMIT:def 9 :

for A being non empty set

for b_{2} being set holds

( b_{2} = MSS_set A iff for x being object holds

( x in b_{2} iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) );

for A being non empty set

for b

( b

( x in b

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) );

registration

let A be non empty set ;

coherence

( not MSS_set A is empty & MSS_set A is MSS-membered )

end;
coherence

( not MSS_set A is empty & MSS_set A is MSS-membered )

proof end;

definition

let A be non empty MSS-membered set ;

:: original: Element

redefine mode Element of A -> non empty non void strict ManySortedSign ;

coherence

for b_{1} being Element of A holds b_{1} is non empty non void strict ManySortedSign
by Def7;

end;
:: original: Element

redefine mode Element of A -> non empty non void strict ManySortedSign ;

coherence

for b

definition

let S1, S2 be ManySortedSign ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) & ( for x being set holds

( x in b_{2} iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) holds

b_{1} = b_{2}

end;
func MSS_morph (S1,S2) -> set means :: MSALIMIT:def 10

for x being set holds

( x in it iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) );

existence for x being set holds

( x in it iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) );

ex b

for x being set holds

( x in b

( x = [f,g] & f,g form_morphism_between S1,S2 ) )

proof end;

uniqueness for b

( x in b

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) & ( for x being set holds

( x in b

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) ) holds

b

proof end;

:: deftheorem defines MSS_morph MSALIMIT:def 10 :

for S1, S2 being ManySortedSign

for b_{3} being set holds

( b_{3} = MSS_morph (S1,S2) iff for x being set holds

( x in b_{3} iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) );

for S1, S2 being ManySortedSign

for b

( b

( x in b

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) );