:: by Andrzej Trybulec

::

:: Received August 7, 2009

:: Copyright (c) 2009-2012 Association of Mizar Users

begin

definition

let D be set ;

let p, q be Element of D * ;

:: original: ^

redefine func p ^ q -> Element of D * ;

coherence

p ^ q is Element of D *

end;
let p, q be Element of D * ;

:: original: ^

redefine func p ^ q -> Element of D * ;

coherence

p ^ q is Element of D *

proof end;

registration

let D be set ;

ex b_{1} being Element of D * st b_{1} is empty

end;
cluster Relation-like NAT -defined D -valued Function-like empty finite countable FinSequence-like FinSubsequence-like for Element of D * ;

existence ex b

proof end;

definition

let D be set ;

:: original: <*>

redefine func <*> D -> empty Element of D * ;

coherence

<*> D is empty Element of D * by FINSEQ_1:def 11;

end;
:: original: <*>

redefine func <*> D -> empty Element of D * ;

coherence

<*> D is empty Element of D * by FINSEQ_1:def 11;

definition

let D be non empty set ;

let d be Element of D;

:: original: <*

redefine func <*d*> -> Element of D * ;

coherence

<*d*> is Element of D *

:: original: <*

redefine func <*d,e*> -> Element of D * ;

coherence

<*d,e*> is Element of D *

end;
let d be Element of D;

:: original: <*

redefine func <*d*> -> Element of D * ;

coherence

<*d*> is Element of D *

proof end;

let e be Element of D;:: original: <*

redefine func <*d,e*> -> Element of D * ;

coherence

<*d,e*> is Element of D *

proof end;

begin

registration
end;

definition

let D be set ;

let F be FinSequence of D * ;

ex b_{1} being Element of D * ex g being BinOp of (D *) st

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b_{1} = g "**" F )

for b_{1}, b_{2} being Element of D * st ex g being BinOp of (D *) st

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b_{1} = g "**" F ) & ex g being BinOp of (D *) st

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b_{2} = g "**" F ) holds

b_{1} = b_{2}

end;
let F be FinSequence of D * ;

func FlattenSeq F -> Element of D * means :Def1: :: PRE_POLY:def 1

ex g being BinOp of (D *) st

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it = g "**" F );

existence ex g being BinOp of (D *) st

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it = g "**" F );

ex b

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b

proof end;

uniqueness for b

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b

b

proof end;

:: deftheorem Def1 defines FlattenSeq PRE_POLY:def 1 :

for D being set

for F being FinSequence of D *

for b_{3} being Element of D * holds

( b_{3} = FlattenSeq F iff ex g being BinOp of (D *) st

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b_{3} = g "**" F ) );

for D being set

for F being FinSequence of D *

for b

( b

( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b

:: from SCMFSA_7, 2006.03.14, A.T.

theorem Th3: :: PRE_POLY:3

for D being set

for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)

for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)

proof end;

:: from SCMFSA_7, 2007.07.22, A.T.

begin

registration
end;

registration
end;

registration

let X be non empty set ;

existence

ex b_{1} being Subset of (Fin X) st

( not b_{1} is empty & b_{1} is with_non-empty_elements )

end;
existence

ex b

( not b

proof end;

registration

let X be non empty set ;

let F be non empty with_non-empty_elements Subset of (Fin X);

existence

not for b_{1} being Element of F holds b_{1} is empty

end;
let F be non empty with_non-empty_elements Subset of (Fin X);

existence

not for b

proof end;

registration

let X be non empty set ;

existence

ex b_{1} being Subset of (Fin X) st b_{1} is with_non-empty_element

end;
existence

ex b

proof end;

definition

let X be non empty set ;

let R be Order of X;

let A be Subset of X;

:: original: |_2

redefine func R |_2 A -> Order of A;

coherence

R |_2 A is Order of A

end;
let R be Order of X;

let A be Subset of X;

:: original: |_2

redefine func R |_2 A -> Order of A;

coherence

R |_2 A is Order of A

proof end;

scheme :: PRE_POLY:sch 2

SubFinite{ F_{1}() -> set , F_{2}() -> Subset of F_{1}(), P_{1}[ set ] } :

provided

SubFinite{ F

provided

A1:
F_{2}() is finite
and

A2: P_{1}[ {} F_{1}()]
and

A3: for x being Element of F_{1}()

for B being Subset of F_{1}() st x in F_{2}() & B c= F_{2}() & P_{1}[B] holds

P_{1}[B \/ {x}]

A2: P

A3: for x being Element of F

for B being Subset of F

P

proof end;

registration

let X be non empty set ;

let F be with_non-empty_element Subset of (Fin X);

existence

ex b_{1} being Element of F st

( b_{1} is finite & not b_{1} is empty )

end;
let F be with_non-empty_element Subset of (Fin X);

existence

ex b

( b

proof end;

definition

let X be set ;

let A be finite Subset of X;

let R be Order of X;

assume A1: R linearly_orders A ;

ex b_{1} being FinSequence of X st

( rng b_{1} = A & ( for n, m being Nat st n in dom b_{1} & m in dom b_{1} & n < m holds

( b_{1} /. n <> b_{1} /. m & [(b_{1} /. n),(b_{1} /. m)] in R ) ) )

for b_{1}, b_{2} being FinSequence of X st rng b_{1} = A & ( for n, m being Nat st n in dom b_{1} & m in dom b_{1} & n < m holds

( b_{1} /. n <> b_{1} /. m & [(b_{1} /. n),(b_{1} /. m)] in R ) ) & rng b_{2} = A & ( for n, m being Nat st n in dom b_{2} & m in dom b_{2} & n < m holds

( b_{2} /. n <> b_{2} /. m & [(b_{2} /. n),(b_{2} /. m)] in R ) ) holds

b_{1} = b_{2}

end;
let A be finite Subset of X;

let R be Order of X;

assume A1: R linearly_orders A ;

func SgmX (R,A) -> FinSequence of X means :Def2: :: PRE_POLY:def 2

( rng it = A & ( for n, m being Nat st n in dom it & m in dom it & n < m holds

( it /. n <> it /. m & [(it /. n),(it /. m)] in R ) ) );

existence ( rng it = A & ( for n, m being Nat st n in dom it & m in dom it & n < m holds

( it /. n <> it /. m & [(it /. n),(it /. m)] in R ) ) );

ex b

( rng b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def2 defines SgmX PRE_POLY:def 2 :

for X being set

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

for b_{4} being FinSequence of X holds

( b_{4} = SgmX (R,A) iff ( rng b_{4} = A & ( for n, m being Nat st n in dom b_{4} & m in dom b_{4} & n < m holds

( b_{4} /. n <> b_{4} /. m & [(b_{4} /. n),(b_{4} /. m)] in R ) ) ) );

for X being set

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

for b

( b

( b

theorem :: PRE_POLY:9

for X being set

for A being finite Subset of X

for R being Order of X

for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds

( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds

f = SgmX (R,A)

for A being finite Subset of X

for R being Order of X

for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds

( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds

f = SgmX (R,A)

proof end;

registration

let X be set ;

let F be non empty Subset of (Fin X);

coherence

for b_{1} being Element of F holds b_{1} is finite
;

end;
let F be non empty Subset of (Fin X);

coherence

for b

definition

let X be set ;

let F be non empty Subset of (Fin X);

:: original: Element

redefine mode Element of F -> Subset of X;

coherence

for b_{1} being Element of F holds b_{1} is Subset of X

end;
let F be non empty Subset of (Fin X);

:: original: Element

redefine mode Element of F -> Subset of X;

coherence

for b

proof end;

theorem Th10: :: PRE_POLY:10

for X being set

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

SgmX (R,A) is one-to-one

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

SgmX (R,A) is one-to-one

proof end;

theorem :: PRE_POLY:11

for X being set

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

len (SgmX (R,A)) = card A

for A being finite Subset of X

for R being Order of X st R linearly_orders A holds

len (SgmX (R,A)) = card A

proof end;

begin

theorem :: PRE_POLY:13

for n being Nat

for M being FinSequence st len M = n + 1 holds

M = (Del (M,(len M))) ^ <*(M . (len M))*>

for M being FinSequence st len M = n + 1 holds

M = (Del (M,(len M))) ^ <*(M . (len M))*>

proof end;

definition

let IT be Function;

end;
attr IT is FinSequence-yielding means :Def3: :: PRE_POLY:def 3

for x being set st x in dom IT holds

IT . x is FinSequence;

for x being set st x in dom IT holds

IT . x is FinSequence;

:: deftheorem Def3 defines FinSequence-yielding PRE_POLY:def 3 :

for IT being Function holds

( IT is FinSequence-yielding iff for x being set st x in dom IT holds

IT . x is FinSequence );

for IT being Function holds

( IT is FinSequence-yielding iff for x being set st x in dom IT holds

IT . x is FinSequence );

definition

let F, G be FinSequence-yielding Function;

ex b_{1} being FinSequence-yielding Function st

( dom b_{1} = (dom F) /\ (dom G) & ( for i being set st i in dom b_{1} holds

for f, g being FinSequence st f = F . i & g = G . i holds

b_{1} . i = f ^ g ) )

for b_{1}, b_{2} being FinSequence-yielding Function st dom b_{1} = (dom F) /\ (dom G) & ( for i being set st i in dom b_{1} holds

for f, g being FinSequence st f = F . i & g = G . i holds

b_{1} . i = f ^ g ) & dom b_{2} = (dom F) /\ (dom G) & ( for i being set st i in dom b_{2} holds

for f, g being FinSequence st f = F . i & g = G . i holds

b_{2} . i = f ^ g ) holds

b_{1} = b_{2}

end;
func F ^^ G -> FinSequence-yielding Function means :Def4: :: PRE_POLY:def 4

( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds

for f, g being FinSequence st f = F . i & g = G . i holds

it . i = f ^ g ) );

existence ( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds

for f, g being FinSequence st f = F . i & g = G . i holds

it . i = f ^ g ) );

ex b

( dom b

for f, g being FinSequence st f = F . i & g = G . i holds

b

proof end;

uniqueness for b

for f, g being FinSequence st f = F . i & g = G . i holds

b

for f, g being FinSequence st f = F . i & g = G . i holds

b

b

proof end;

:: deftheorem Def4 defines ^^ PRE_POLY:def 4 :

for F, G, b_{3} being FinSequence-yielding Function holds

( b_{3} = F ^^ G iff ( dom b_{3} = (dom F) /\ (dom G) & ( for i being set st i in dom b_{3} holds

for f, g being FinSequence st f = F . i & g = G . i holds

b_{3} . i = f ^ g ) ) );

for F, G, b

( b

for f, g being FinSequence st f = F . i & g = G . i holds

b

begin

theorem :: PRE_POLY:15

for V, C being set

for f being Element of PFuncs (V,C)

for g being set st g c= f holds

g in PFuncs (V,C)

for f being Element of PFuncs (V,C)

for g being set st g c= f holds

g in PFuncs (V,C)

proof end;

registration

existence

ex b_{1} being set st

( b_{1} is functional & b_{1} is finite & not b_{1} is empty )

end;
ex b

( b

proof end;

begin

registration

let D be set ;

coherence

for b_{1} being FinSequence of D * holds b_{1} is FinSequence-yielding

end;
coherence

for b

proof end;

registration

coherence

for b_{1} being Function st b_{1} is FinSequence-yielding holds

b_{1} is Function-yielding

end;
for b

b

proof end;

begin

registration

let X be set ;

let f be ManySortedSet of X;

let x, y be set ;

coherence

f +* (x,y) is X -defined

end;
let f be ManySortedSet of X;

let x, y be set ;

coherence

f +* (x,y) is X -defined

proof end;

registration

let X be set ;

let f be ManySortedSet of X;

let x, y be set ;

coherence

for b_{1} being X -defined Function st b_{1} = f +* (x,y) holds

b_{1} is total

end;
let f be ManySortedSet of X;

let x, y be set ;

coherence

for b

b

proof end;

definition

let A, X be set ;

let D be non empty FinSequenceSet of A;

let p be PartFunc of X,D;

let i be set ;

:: original: /.

redefine func p /. i -> Element of D;

coherence

p /. i is Element of D ;

end;
let D be non empty FinSequenceSet of A;

let p be PartFunc of X,D;

let i be set ;

:: original: /.

redefine func p /. i -> Element of D;

coherence

p /. i is Element of D ;

registration

let X be set ;

ex b_{1} being Order of X st

( b_{1} is being_linear-order & b_{1} is well-ordering )

end;
cluster Relation-like X -defined X -valued total quasi_total reflexive antisymmetric transitive well-ordering being_linear-order for Element of bool [:X,X:];

existence ex b

( b

proof end;

theorem Th20: :: PRE_POLY:20

for X being non empty set

for A being non empty finite Subset of X

for R being Order of X

for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds

[x,y] in R ) holds

(SgmX (R,A)) /. 1 = x

for A being non empty finite Subset of X

for R being Order of X

for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds

[x,y] in R ) holds

(SgmX (R,A)) /. 1 = x

proof end;

theorem Th21: :: PRE_POLY:21

for X being non empty set

for A being non empty finite Subset of X

for R being Order of X

for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds

[y,x] in R ) holds

(SgmX (R,A)) /. (len (SgmX (R,A))) = x

for A being non empty finite Subset of X

for R being Order of X

for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds

[y,x] in R ) holds

(SgmX (R,A)) /. (len (SgmX (R,A))) = x

proof end;

registration

let X be non empty set ;

let A be non empty finite Subset of X;

let R be being_linear-order Order of X;

coherence

( not SgmX (R,A) is empty & SgmX (R,A) is one-to-one )

end;
let A be non empty finite Subset of X;

let R be being_linear-order Order of X;

coherence

( not SgmX (R,A) is empty & SgmX (R,A) is one-to-one )

proof end;

registration
end;

registration
end;

registration
end;

registration

let F be FinSequence-yielding FinSequence;

let x be set ;

coherence

F . x is FinSequence-like

end;
let x be set ;

coherence

F . x is FinSequence-like

proof end;

registration

ex b_{1} being FinSequence st b_{1} is Cardinal-yielding
end;

cluster Relation-like NAT -defined Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like for set ;

existence ex b

proof end;

theorem Th22: :: PRE_POLY:22

for f being Function holds

( f is Cardinal-yielding iff for y being set st y in rng f holds

y is Cardinal )

( f is Cardinal-yielding iff for y being set st y in rng f holds

y is Cardinal )

proof end;

registration
end;

registration
end;

registration

ex b_{1} being FinSequence of NAT st b_{1} is Cardinal-yielding
end;

cluster Relation-like NAT -defined NAT -valued Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued for FinSequence of NAT ;

existence ex b

proof end;

definition

let D be set ;

let F be FinSequence of D * ;

:: original: Card

redefine func Card F -> Cardinal-yielding FinSequence of NAT ;

coherence

Card F is Cardinal-yielding FinSequence of NAT

end;
let F be FinSequence of D * ;

:: original: Card

redefine func Card F -> Cardinal-yielding FinSequence of NAT ;

coherence

Card F is Cardinal-yielding FinSequence of NAT

proof end;

registration
end;

registration
end;

registration
end;

theorem Th26: :: PRE_POLY:26

for f being Function holds

( f is FinSequence-yielding iff for y being set st y in rng f holds

y is FinSequence )

( f is FinSequence-yielding iff for y being set st y in rng f holds

y is FinSequence )

proof end;

registration
end;

registration
end;

theorem Th28: :: PRE_POLY:28

for D, E being set

for F being FinSequence of D *

for G being FinSequence of E * st Card F = Card G holds

len (FlattenSeq F) = len (FlattenSeq G)

for F being FinSequence of D *

for G being FinSequence of E * st Card F = Card G holds

len (FlattenSeq F) = len (FlattenSeq G)

proof end;

theorem Th29: :: PRE_POLY:29

for D being set

for F being FinSequence of D *

for k being set st k in dom (FlattenSeq F) holds

ex i, j being Element of NAT st

( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k )

for F being FinSequence of D *

for k being set st k in dom (FlattenSeq F) holds

ex i, j being Element of NAT st

( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k )

proof end;

theorem Th30: :: PRE_POLY:30

for D being set

for F being FinSequence of D *

for i, j being Element of NAT st i in dom F & j in dom (F . i) holds

( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) )

for F being FinSequence of D *

for i, j being Element of NAT st i in dom F & j in dom (F . i) holds

( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) )

proof end;

theorem Th31: :: PRE_POLY:31

for X, Y being non empty set

for f being FinSequence of X *

for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y *

for f being FinSequence of X *

for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y *

proof end;

theorem :: PRE_POLY:32

for X, Y being non empty set

for f being FinSequence of X *

for v being Function of X,Y ex F being FinSequence of Y * st

( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )

for f being FinSequence of X *

for v being Function of X,Y ex F being FinSequence of Y * st

( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )

proof end;

begin

registration

let f be natural-valued Function;

let x be set ;

let n be Nat;

coherence

f +* (x,n) is natural-valued

end;
let x be set ;

let n be Nat;

coherence

f +* (x,n) is natural-valued

proof end;

registration

let f be real-valued Function;

let x be set ;

let n be real number ;

coherence

f +* (x,n) is real-valued

end;
let x be set ;

let n be real number ;

coherence

f +* (x,n) is real-valued

proof end;

definition

let X be set ;

let b1, b2 be complex-valued ManySortedSet of X;

b1 + b2 is ManySortedSet of X ;

compatibility

for b_{1} being ManySortedSet of X holds

( b_{1} = b1 + b2 iff for x being set holds b_{1} . x = (b1 . x) + (b2 . x) )

end;
let b1, b2 be complex-valued ManySortedSet of X;

:: original: +

redefine func b1 + b2 -> ManySortedSet of X means :Def5: :: PRE_POLY:def 5

for x being set holds it . x = (b1 . x) + (b2 . x);

coherence redefine func b1 + b2 -> ManySortedSet of X means :Def5: :: PRE_POLY:def 5

for x being set holds it . x = (b1 . x) + (b2 . x);

b1 + b2 is ManySortedSet of X ;

compatibility

for b

( b

proof end;

:: deftheorem Def5 defines + PRE_POLY:def 5 :

for X being set

for b1, b2 being complex-valued ManySortedSet of X

for b_{4} being ManySortedSet of X holds

( b_{4} = b1 + b2 iff for x being set holds b_{4} . x = (b1 . x) + (b2 . x) );

for X being set

for b1, b2 being complex-valued ManySortedSet of X

for b

( b

definition

let X be set ;

let b1, b2 be natural-valued ManySortedSet of X;

ex b_{1} being ManySortedSet of X st

for x being set holds b_{1} . x = (b1 . x) -' (b2 . x)

for b_{1}, b_{2} being ManySortedSet of X st ( for x being set holds b_{1} . x = (b1 . x) -' (b2 . x) ) & ( for x being set holds b_{2} . x = (b1 . x) -' (b2 . x) ) holds

b_{1} = b_{2}

end;
let b1, b2 be natural-valued ManySortedSet of X;

func b1 -' b2 -> ManySortedSet of X means :Def6: :: PRE_POLY:def 6

for x being set holds it . x = (b1 . x) -' (b2 . x);

existence for x being set holds it . x = (b1 . x) -' (b2 . x);

ex b

for x being set holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines -' PRE_POLY:def 6 :

for X being set

for b1, b2 being natural-valued ManySortedSet of X

for b_{4} being ManySortedSet of X holds

( b_{4} = b1 -' b2 iff for x being set holds b_{4} . x = (b1 . x) -' (b2 . x) );

for X being set

for b1, b2 being natural-valued ManySortedSet of X

for b

( b

theorem :: PRE_POLY:33

for X being set

for b, b1, b2 being real-valued ManySortedSet of X st ( for x being set st x in X holds

b . x = (b1 . x) + (b2 . x) ) holds

b = b1 + b2

for b, b1, b2 being real-valued ManySortedSet of X st ( for x being set st x in X holds

b . x = (b1 . x) + (b2 . x) ) holds

b = b1 + b2

proof end;

theorem Th34: :: PRE_POLY:34

for X being set

for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being set st x in X holds

b . x = (b1 . x) -' (b2 . x) ) holds

b = b1 -' b2

for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being set st x in X holds

b . x = (b1 . x) -' (b2 . x) ) holds

b = b1 -' b2

proof end;

registration

let X be set ;

let b1, b2 be natural-valued ManySortedSet of X;

coherence

b1 + b2 is natural-valued ;

coherence

b1 -' b2 is natural-valued

end;
let b1, b2 be natural-valued ManySortedSet of X;

coherence

b1 + b2 is natural-valued ;

coherence

b1 -' b2 is natural-valued

proof end;

theorem Th35: :: PRE_POLY:35

for X being set

for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)

for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)

proof end;

theorem :: PRE_POLY:36

for X being set

for b, c, d being natural-valued ManySortedSet of X holds (b -' c) -' d = b -' (c + d)

for b, c, d being natural-valued ManySortedSet of X holds (b -' c) -' d = b -' (c + d)

proof end;

begin

definition

let f be Function;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff f . x <> 0 )

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

( x in b_{1} iff f . x <> 0 ) ) & ( for x being set holds

( x in b_{2} iff f . x <> 0 ) ) holds

b_{1} = b_{2}

end;
func support f -> set means :Def7: :: PRE_POLY:def 7

for x being set holds

( x in it iff f . x <> 0 );

existence for x being set holds

( x in it iff f . x <> 0 );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines support PRE_POLY:def 7 :

for f being Function

for b_{2} being set holds

( b_{2} = support f iff for x being set holds

( x in b_{2} iff f . x <> 0 ) );

for f being Function

for b

( b

( x in b

definition
end;

:: deftheorem Def8 defines finite-support PRE_POLY:def 8 :

for f being Function holds

( f is finite-support iff support f is finite );

for f being Function holds

( f is finite-support iff support f is finite );

registration
end;

registration

existence

ex b_{1} being Function st

( b_{1} is natural-valued & b_{1} is finite-support & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

let X be set ;

ex b_{1} being Function of X,NAT st b_{1} is finite-support

end;
cluster Relation-like X -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued finite-support for Element of bool [:X,NAT:];

existence ex b

proof end;

registration

let f be finite-support Function;

let x, y be set ;

coherence

f +* (x,y) is finite-support

end;
let x, y be set ;

coherence

f +* (x,y) is finite-support

proof end;

registration

let X be set ;

existence

ex b_{1} being ManySortedSet of X st

( b_{1} is natural-valued & b_{1} is finite-support )

end;
existence

ex b

( b

proof end;

theorem Th38: :: PRE_POLY:38

for X being set

for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2)

for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2)

proof end;

theorem Th39: :: PRE_POLY:39

for X being set

for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1

for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1

proof end;

begin

registration

let X be finite set ;

coherence

for b_{1} being ManySortedSet of X holds b_{1} is finite-support

end;
coherence

for b

proof end;

registration

let X be set ;

let b1, b2 be bag of X;

coherence

b1 + b2 is finite-support

b1 -' b2 is finite-support

end;
let b1, b2 be bag of X;

coherence

b1 + b2 is finite-support

proof end;

coherence b1 -' b2 is finite-support

proof end;

definition

let n be Ordinal;

let p, q be bag of n;

for p, q being bag of n st ex k being Ordinal st

( p . k < q . k & ( for l being Ordinal st l in k holds

p . l = q . l ) ) holds

for k being Ordinal holds

( not q . k < p . k or ex l being Ordinal st

( l in k & not q . l = p . l ) )

end;
let p, q be bag of n;

pred p < q means :Def9: :: PRE_POLY:def 9

ex k being Ordinal st

( p . k < q . k & ( for l being Ordinal st l in k holds

p . l = q . l ) );

asymmetry ex k being Ordinal st

( p . k < q . k & ( for l being Ordinal st l in k holds

p . l = q . l ) );

for p, q being bag of n st ex k being Ordinal st

( p . k < q . k & ( for l being Ordinal st l in k holds

p . l = q . l ) ) holds

for k being Ordinal holds

( not q . k < p . k or ex l being Ordinal st

( l in k & not q . l = p . l ) )

proof end;

:: deftheorem Def9 defines < PRE_POLY:def 9 :

for n being Ordinal

for p, q being bag of n holds

( p < q iff ex k being Ordinal st

( p . k < q . k & ( for l being Ordinal st l in k holds

p . l = q . l ) ) );

for n being Ordinal

for p, q being bag of n holds

( p < q iff ex k being Ordinal st

( p . k < q . k & ( for l being Ordinal st l in k holds

p . l = q . l ) ) );

definition
end;

:: deftheorem Def10 defines <=' PRE_POLY:def 10 :

for n being Ordinal

for p, q being bag of n holds

( p <=' q iff ( p < q or p = q ) );

for n being Ordinal

for p, q being bag of n holds

( p <=' q iff ( p < q or p = q ) );

definition

let X be set ;

let d, b be bag of X;

reflexivity

for d being bag of X

for k being set holds d . k <= d . k ;

end;
let d, b be bag of X;

reflexivity

for d being bag of X

for k being set holds d . k <= d . k ;

:: deftheorem Def11 defines divides PRE_POLY:def 11 :

for X being set

for d, b being bag of X holds

( d divides b iff for k being set holds d . k <= b . k );

for X being set

for d, b being bag of X holds

( d divides b iff for k being set holds d . k <= b . k );

theorem Th46: :: PRE_POLY:46

for n being set

for d, b being bag of n st ( for k being set st k in n holds

d . k <= b . k ) holds

d divides b

for d, b being bag of n st ( for k being set st k in n holds

d . k <= b . k ) holds

d divides b

proof end;

definition

let X be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is bag of X )

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

( x in b_{1} iff x is bag of X ) ) & ( for x being set holds

( x in b_{2} iff x is bag of X ) ) holds

b_{1} = b_{2}

end;
func Bags X -> set means :Def12: :: PRE_POLY:def 12

for x being set holds

( x in it iff x is bag of X );

existence for x being set holds

( x in it iff x is bag of X );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def12 defines Bags PRE_POLY:def 12 :

for X being set

for b_{2} being set holds

( b_{2} = Bags X iff for x being set holds

( x in b_{2} iff x is bag of X ) );

for X being set

for b

( b

( x in b

definition

let X be set ;

:: original: Bags

redefine func Bags X -> Subset of (Bags X);

coherence

Bags X is Subset of (Bags X)

end;
:: original: Bags

redefine func Bags X -> Subset of (Bags X);

coherence

Bags X is Subset of (Bags X)

proof end;

registration
end;

registration
end;

registration

let X be set ;

let B be Subset of (Bags X);

coherence

for b_{1} being Element of B holds b_{1} is X -defined

end;
let B be Subset of (Bags X);

coherence

for b

proof end;

registration

let X be set ;

let B be non empty Subset of (Bags X);

coherence

for b_{1} being Element of B holds

( b_{1} is total & b_{1} is natural-valued & b_{1} is finite-support )
by Def12;

end;
let B be non empty Subset of (Bags X);

coherence

for b

( b

theorem :: PRE_POLY:60

definition

let n be Ordinal;

ex b_{1} being Order of (Bags n) st

for p, q being bag of n holds

( [p,q] in b_{1} iff p <=' q )

for b_{1}, b_{2} being Order of (Bags n) st ( for p, q being bag of n holds

( [p,q] in b_{1} iff p <=' q ) ) & ( for p, q being bag of n holds

( [p,q] in b_{2} iff p <=' q ) ) holds

b_{1} = b_{2}

end;
func BagOrder n -> Order of (Bags n) means :Def14: :: PRE_POLY:def 14

for p, q being bag of n holds

( [p,q] in it iff p <=' q );

existence for p, q being bag of n holds

( [p,q] in it iff p <=' q );

ex b

for p, q being bag of n holds

( [p,q] in b

proof end;

uniqueness for b

( [p,q] in b

( [p,q] in b

b

proof end;

:: deftheorem Def14 defines BagOrder PRE_POLY:def 14 :

for n being Ordinal

for b_{2} being Order of (Bags n) holds

( b_{2} = BagOrder n iff for p, q being bag of n holds

( [p,q] in b_{2} iff p <=' q ) );

for n being Ordinal

for b

( b

( [p,q] in b

Lm1: for n being Ordinal holds BagOrder n is_reflexive_in Bags n

proof end;

Lm2: for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n

proof end;

Lm3: for n being Ordinal holds BagOrder n is_transitive_in Bags n

proof end;

Lm4: for n being Ordinal holds BagOrder n linearly_orders Bags n

proof end;

definition

let X be set ;

let f be Function of X,NAT;

ex b_{1} being Subset of (Funcs (X,NAT)) st

for g being natural-valued ManySortedSet of X holds

( g in b_{1} iff for x being set st x in X holds

g . x <= f . x )

for b_{1}, b_{2} being Subset of (Funcs (X,NAT)) st ( for g being natural-valued ManySortedSet of X holds

( g in b_{1} iff for x being set st x in X holds

g . x <= f . x ) ) & ( for g being natural-valued ManySortedSet of X holds

( g in b_{2} iff for x being set st x in X holds

g . x <= f . x ) ) holds

b_{1} = b_{2}

end;
let f be Function of X,NAT;

func NatMinor f -> Subset of (Funcs (X,NAT)) means :Def15: :: PRE_POLY:def 15

for g being natural-valued ManySortedSet of X holds

( g in it iff for x being set st x in X holds

g . x <= f . x );

existence for g being natural-valued ManySortedSet of X holds

( g in it iff for x being set st x in X holds

g . x <= f . x );

ex b

for g being natural-valued ManySortedSet of X holds

( g in b

g . x <= f . x )

proof end;

uniqueness for b

( g in b

g . x <= f . x ) ) & ( for g being natural-valued ManySortedSet of X holds

( g in b

g . x <= f . x ) ) holds

b

proof end;

:: deftheorem Def15 defines NatMinor PRE_POLY:def 15 :

for X being set

for f being Function of X,NAT

for b_{3} being Subset of (Funcs (X,NAT)) holds

( b_{3} = NatMinor f iff for g being natural-valued ManySortedSet of X holds

( g in b_{3} iff for x being set st x in X holds

g . x <= f . x ) );

for X being set

for f being Function of X,NAT

for b

( b

( g in b

g . x <= f . x ) );

registration

let X be set ;

let f be Function of X,NAT;

coherence

( not NatMinor f is empty & NatMinor f is functional ) by Th61;

end;
let f be Function of X,NAT;

coherence

( not NatMinor f is empty & NatMinor f is functional ) by Th61;

registration

let X be set ;

let f be Function of X,NAT;

coherence

for b_{1} being Element of NatMinor f holds b_{1} is natural-valued

end;
let f be Function of X,NAT;

coherence

for b

proof end;

definition

let X be set ;

let f be finite-support Function of X,NAT;

:: original: support

redefine func support f -> Element of Fin X;

coherence

support f is Element of Fin X

end;
let f be finite-support Function of X,NAT;

:: original: support

redefine func support f -> Element of Fin X;

coherence

support f is Element of Fin X

proof end;

theorem Th63: :: PRE_POLY:63

for X being non empty set

for f being finite-support Function of X,NAT holds card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1)))

for f being finite-support Function of X,NAT holds card (NatMinor f) = multnat $$ ((support f),(addnat [:] (f,1)))

proof end;

registration
end;

definition

let n be Ordinal;

let b be bag of n;

ex b_{1} being FinSequence of Bags n ex S being non empty finite Subset of (Bags n) st

( b_{1} = SgmX ((BagOrder n),S) & ( for p being bag of n holds

( p in S iff p divides b ) ) )

for b_{1}, b_{2} being FinSequence of Bags n st ex S being non empty finite Subset of (Bags n) st

( b_{1} = SgmX ((BagOrder n),S) & ( for p being bag of n holds

( p in S iff p divides b ) ) ) & ex S being non empty finite Subset of (Bags n) st

( b_{2} = SgmX ((BagOrder n),S) & ( for p being bag of n holds

( p in S iff p divides b ) ) ) holds

b_{1} = b_{2}

end;
let b be bag of n;

func divisors b -> FinSequence of Bags n means :Def16: :: PRE_POLY:def 16

ex S being non empty finite Subset of (Bags n) st

( it = SgmX ((BagOrder n),S) & ( for p being bag of n holds

( p in S iff p divides b ) ) );

existence ex S being non empty finite Subset of (Bags n) st

( it = SgmX ((BagOrder n),S) & ( for p being bag of n holds

( p in S iff p divides b ) ) );

ex b

( b

( p in S iff p divides b ) ) )

proof end;

uniqueness for b

( b

( p in S iff p divides b ) ) ) & ex S being non empty finite Subset of (Bags n) st

( b

( p in S iff p divides b ) ) ) holds

b

proof end;

:: deftheorem Def16 defines divisors PRE_POLY:def 16 :

for n being Ordinal

for b being bag of n

for b_{3} being FinSequence of Bags n holds

( b_{3} = divisors b iff ex S being non empty finite Subset of (Bags n) st

( b_{3} = SgmX ((BagOrder n),S) & ( for p being bag of n holds

( p in S iff p divides b ) ) ) );

for n being Ordinal

for b being bag of n

for b

( b

( b

( p in S iff p divides b ) ) ) );

registration

let n be Ordinal;

let b be bag of n;

coherence

( not divisors b is empty & divisors b is one-to-one )

end;
let b be bag of n;

coherence

( not divisors b is empty & divisors b is one-to-one )

proof end;

theorem Th64: :: PRE_POLY:64

for n being Ordinal

for i being Element of NAT

for b being bag of n st i in dom (divisors b) holds

(divisors b) /. i divides b

for i being Element of NAT

for b being bag of n st i in dom (divisors b) holds

(divisors b) /. i divides b

proof end;

theorem Th65: :: PRE_POLY:65

for n being Ordinal

for b being bag of n holds

( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )

for b being bag of n holds

( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )

proof end;

theorem Th66: :: PRE_POLY:66

for n being Ordinal

for i being Nat

for b, b1, b2 being bag of n st i > 1 & i < len (divisors b) holds

( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )

for i being Nat

for b, b1, b2 being bag of n st i > 1 & i < len (divisors b) holds

( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )

proof end;

definition

let n be Ordinal;

let b be bag of n;

ex b_{1} being FinSequence of 2 -tuples_on (Bags n) st

( dom b_{1} = dom (divisors b) & ( for i being Element of NAT

for p being bag of n st i in dom b_{1} & p = (divisors b) /. i holds

b_{1} /. i = <*p,(b -' p)*> ) )

for b_{1}, b_{2} being FinSequence of 2 -tuples_on (Bags n) st dom b_{1} = dom (divisors b) & ( for i being Element of NAT

for p being bag of n st i in dom b_{1} & p = (divisors b) /. i holds

b_{1} /. i = <*p,(b -' p)*> ) & dom b_{2} = dom (divisors b) & ( for i being Element of NAT

for p being bag of n st i in dom b_{2} & p = (divisors b) /. i holds

b_{2} /. i = <*p,(b -' p)*> ) holds

b_{1} = b_{2}

end;
let b be bag of n;

func decomp b -> FinSequence of 2 -tuples_on (Bags n) means :Def17: :: PRE_POLY:def 17

( dom it = dom (divisors b) & ( for i being Element of NAT

for p being bag of n st i in dom it & p = (divisors b) /. i holds

it /. i = <*p,(b -' p)*> ) );

existence ( dom it = dom (divisors b) & ( for i being Element of NAT

for p being bag of n st i in dom it & p = (divisors b) /. i holds

it /. i = <*p,(b -' p)*> ) );

ex b

( dom b

for p being bag of n st i in dom b

b

proof end;

uniqueness for b

for p being bag of n st i in dom b

b

for p being bag of n st i in dom b

b

b

proof end;

:: deftheorem Def17 defines decomp PRE_POLY:def 17 :

for n being Ordinal

for b being bag of n

for b_{3} being FinSequence of 2 -tuples_on (Bags n) holds

( b_{3} = decomp b iff ( dom b_{3} = dom (divisors b) & ( for i being Element of NAT

for p being bag of n st i in dom b_{3} & p = (divisors b) /. i holds

b_{3} /. i = <*p,(b -' p)*> ) ) );

for n being Ordinal

for b being bag of n

for b

( b

for p being bag of n st i in dom b

b

theorem Th68: :: PRE_POLY:68

for n being Ordinal

for i being Element of NAT

for b being bag of n st i in dom (decomp b) holds

ex b1, b2 being bag of n st

( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )

for i being Element of NAT

for b being bag of n st i in dom (decomp b) holds

ex b1, b2 being bag of n st

( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )

proof end;

theorem Th69: :: PRE_POLY:69

for n being Ordinal

for b, b1, b2 being bag of n st b = b1 + b2 holds

ex i being Element of NAT st

( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )

for b, b1, b2 being bag of n st b = b1 + b2 holds

ex i being Element of NAT st

( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )

proof end;

theorem Th70: :: PRE_POLY:70

for n being Ordinal

for i being Element of NAT

for b, b1, b2 being bag of n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds

b1 = (divisors b) /. i

for i being Element of NAT

for b, b1, b2 being bag of n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds

b1 = (divisors b) /. i

proof end;

registration

let n be Ordinal;

let b be bag of n;

coherence

( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding )

end;
let b be bag of n;

coherence

( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding )

proof end;

registration

let n be Ordinal;

let b be Element of Bags n;

coherence

( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding ) ;

end;
let b be Element of Bags n;

coherence

( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding ) ;

theorem :: PRE_POLY:71

for n being Ordinal

for b being bag of n holds

( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> )

for b being bag of n holds

( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> )

proof end;

theorem :: PRE_POLY:72

for n being Ordinal

for i being Nat

for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds

( b1 <> EmptyBag n & b2 <> EmptyBag n )

for i being Nat

for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds

( b1 <> EmptyBag n & b2 <> EmptyBag n )

proof end;

theorem :: PRE_POLY:74

for n being Ordinal

for b being bag of n

for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds

f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds

g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds

ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p

for b being bag of n

for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds

f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds

g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds

ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq g = (FlattenSeq f) * p

proof end;

theorem :: PRE_POLY:75

for X being set

for b1, b2 being real-valued ManySortedSet of X holds support (b1 + b2) c= (support b1) \/ (support b2)

for b1, b2 being real-valued ManySortedSet of X holds support (b1 + b2) c= (support b1) \/ (support b2)

proof end;

registration

let D be non empty set ;

let n be Element of NAT ;

coherence

for b_{1} being FinSequence of n -tuples_on D holds b_{1} is FinSequence-yielding

end;
let n be Element of NAT ;

coherence

for b

proof end;

registration

let k be Element of NAT ;

let D be non empty set ;

let M be FinSequence of k -tuples_on D;

let x be set ;

coherence

( M /. x is Function-like & M /. x is Relation-like ) ;

end;
let D be non empty set ;

let M be FinSequence of k -tuples_on D;

let x be set ;

coherence

( M /. x is Function-like & M /. x is Relation-like ) ;

registration

let k be Element of NAT ;

let D be non empty set ;

let M be FinSequence of k -tuples_on D;

let x be set ;

coherence

( M /. x is D -valued & M /. x is FinSequence-like ) ;

end;
let D be non empty set ;

let M be FinSequence of k -tuples_on D;

let x be set ;

coherence

( M /. x is D -valued & M /. x is FinSequence-like ) ;