begin
scheme
FinRecUnD2{
F1()
-> set ,
F2()
-> Element of
F1(),
F3()
-> Element of
NAT ,
F4()
-> FinSequence of
F1(),
F5()
-> FinSequence of
F1(),
P1[
set ,
set ,
set ] } :
provided
A1:
for
n being
Element of
NAT st 1
<= n &
n <= F3()
- 1 holds
for
x,
y1,
y2 being
Element of
F1() st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2
and A2:
(
len F4()
= F3() & (
F4()
/. 1
= F2() or
F3()
= 0 ) & ( for
n being
Element of
NAT st 1
<= n &
n <= F3()
- 1 holds
P1[
n,
F4()
/. n,
F4()
/. (n + 1)] ) )
and A3:
(
len F5()
= F3() & (
F5()
/. 1
= F2() or
F3()
= 0 ) & ( for
n being
Element of
NAT st 1
<= n &
n <= F3()
- 1 holds
P1[
n,
F5()
/. n,
F5()
/. (n + 1)] ) )
Lm1:
for X being set
for A being Subset of X
for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )
Lm2:
for X being set
for A being Subset of X
for O being Order of X st O is_connected_in X holds
O is_connected_in A
Lm3:
for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S
theorem
canceled;
theorem Th2:
begin
theorem
canceled;
theorem Th4:
Lm4:
for X being set
for A being finite Subset of X
for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
Lm5:
for D being set
for p being FinSequence of D st dom p <> {} holds
1 in dom p
theorem Th11:
theorem Th12:
theorem Th13:
begin
theorem Th14:
Lm6:
for X being set
for b being bag of X holds b is PartFunc of X,NAT
:: deftheorem Def1 defines empty POLYNOM2:def 1 :
theorem Th15:
definition
let n be
Ordinal;
let b be
bag of
n;
let L be non
empty non
trivial well-unital doubleLoopStr ;
let x be
Function of
n,
L;
func eval b,
x -> Element of
L means :
Def2:
ex
y being
FinSequence of the
carrier of
L st
(
len y = len (SgmX (RelIncl n),(support b)) &
it = Product y & ( for
i being
Element of
NAT st 1
<= i &
i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),
((b * (SgmX (RelIncl n),(support b))) /. i) ) );
existence
ex b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & b1 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),((b * (SgmX (RelIncl n),(support b))) /. i) ) )
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & b1 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),((b * (SgmX (RelIncl n),(support b))) /. i) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & b2 = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (power L) . ((x * (SgmX (RelIncl n),(support b))) /. i),((b * (SgmX (RelIncl n),(support b))) /. i) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines eval POLYNOM2:def 2 :
Lm7:
for X being set holds support (EmptyBag X) = {}
theorem Th16:
theorem Th17:
Lm8:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr
for b1, b2 being bag of n
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = (power L) . (x . u),(b2 . u) holds
eval b2,x = a * (eval b1,x)
Lm9:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1 being bag of n st ex u being set st support b1 = {u} holds
for b2 being bag of n
for x being Function of n,L holds eval (b1 + b2),x = (eval b1,x) * (eval b2,x)
theorem Th18:
begin
theorem Th19:
theorem Th20:
:: deftheorem defines @ POLYNOM2:def 3 :
definition
let n be
Ordinal;
let L be non
empty non
trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let p be
Polynomial of
n,
L;
let x be
Function of
n,
L;
func eval p,
x -> Element of
L means :
Def4:
ex
y being
FinSequence of the
carrier of
L st
(
len y = len (SgmX (BagOrder n),(Support p)) &
it = Sum y & ( for
i being
Element of
NAT st 1
<= i &
i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) );
existence
ex b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & b1 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) )
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & b1 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) & ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & b2 = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines eval POLYNOM2:def 4 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm10:
for n being Ordinal
for L being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval q,x = (eval p,x) + ((q . b) * (eval b,x))
Lm11:
for n being Ordinal
for L being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L st ex b being bag of n st Support p = {b} holds
for q being Polynomial of n,L
for x being Function of n,L holds eval (p + q),x = (eval p,x) + (eval q,x)
theorem Th25:
theorem
Lm12:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
Lm13:
for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for q being Polynomial of n,L st ex b being bag of n st Support q = {b} holds
for p being Polynomial of n,L
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
theorem Th27:
begin
definition
let n be
Ordinal;
let L be non
empty non
trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let x be
Function of
n,
L;
func Polynom-Evaluation n,
L,
x -> Function of
(Polynom-Ring n,L),
L means :
Def5:
for
p being
Polynomial of
n,
L holds
it . p = eval p,
x;
existence
ex b1 being Function of (Polynom-Ring n,L),L st
for p being Polynomial of n,L holds b1 . p = eval p,x
uniqueness
for b1, b2 being Function of (Polynom-Ring n,L),L st ( for p being Polynomial of n,L holds b1 . p = eval p,x ) & ( for p being Polynomial of n,L holds b2 . p = eval p,x ) holds
b1 = b2
end;
:: deftheorem Def5 defines Polynom-Evaluation POLYNOM2:def 5 :