let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for c being ConstPoly of n,L
for x being Function of n,L holds eval (c,x) = coefficient c

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for c being ConstPoly of n,L
for x being Function of n,L holds eval (c,x) = coefficient c

let c be ConstPoly of n,L; :: thesis: for x being Function of n,L holds eval (c,x) = coefficient c
let x be Function of n,L; :: thesis: eval (c,x) = coefficient c
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((),())) and
A2: eval (c,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((c * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) by POLYNOM2:def 4;
now :: thesis: ( ( coefficient c = 0. L & eval (c,x) = coefficient c ) or ( coefficient c <> 0. L & eval (c,x) = coefficient c ) )
per cases ;
case A4: coefficient c = 0. L ; :: thesis: eval (c,x) = coefficient c
Support c = {}
proof
set u = the Element of Support c;
assume A5: Support c <> {} ; :: thesis: contradiction
then the Element of Support c in Support c ;
then reconsider u = the Element of Support c as Element of Bags n ;
c . u <> 0. L by ;
then u <> EmptyBag n by ;
then c . u = 0. L by Def7;
hence contradiction by A5, POLYNOM1:def 4; :: thesis: verum
end;
then reconsider Sc = Support c as empty Subset of (Bags n) ;
SgmX ((),Sc) = {} by ;
then y = <*> the carrier of L by A1;
hence eval (c,x) = coefficient c by ; :: thesis: verum
end;
case A6: coefficient c <> 0. L ; :: thesis: eval (c,x) = coefficient c
reconsider sc = Support c as finite Subset of (Bags n) ;
set sg = SgmX ((),sc);
A7: BagOrder n linearly_orders sc by POLYNOM2:18;
A8: for u being object st u in Support c holds
u in {()}
proof
let u be object ; :: thesis: ( u in Support c implies u in {()} )
assume A9: u in Support c ; :: thesis: u in {()}
assume A10: not u in {()} ; :: thesis: contradiction
reconsider u = u as Element of Bags n by A9;
u <> EmptyBag n by ;
then c . u = 0. L by Def7;
hence contradiction by A9, POLYNOM1:def 4; :: thesis: verum
end;
for u being object st u in {()} holds
u in Support c
proof
let u be object ; :: thesis: ( u in {()} implies u in Support c )
assume A11: u in {()} ; :: thesis:
then A12: u = EmptyBag n by TARSKI:def 1;
reconsider u = u as Element of Bags n by A11;
c . u <> 0. L by A6, A12, Lm2;
hence u in Support c by POLYNOM1:def 4; :: thesis: verum
end;
then Support c = {()} by ;
then A13: rng (SgmX ((),sc)) = {()} by ;
then A14: EmptyBag n in rng (SgmX ((),sc)) by TARSKI:def 1;
then A15: 1 in dom (SgmX ((),sc)) by FINSEQ_3:31;
then A16: (SgmX ((),sc)) . 1 in rng (SgmX ((),sc)) by FUNCT_1:3;
A17: for u being object st u in dom (SgmX ((),sc)) holds
u in {1}
proof
let u be object ; :: thesis: ( u in dom (SgmX ((),sc)) implies u in {1} )
assume A18: u in dom (SgmX ((),sc)) ; :: thesis: u in {1}
assume A19: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A18;
(SgmX ((),sc)) /. u = (SgmX ((),sc)) . u by ;
then A20: (SgmX ((),sc)) /. u in rng (SgmX ((),sc)) by ;
A21: u <> 1 by ;
A22: 1 < u
proof
consider k being Nat such that
A23: dom (SgmX ((),sc)) = Seg k by FINSEQ_1:def 2;
Seg k = { m where m is Nat : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;
then ex m9 being Nat st
( m9 = u & 1 <= m9 & m9 <= k ) by ;
hence 1 < u by ; :: thesis: verum
end;
(SgmX ((),sc)) /. 1 = (SgmX ((),sc)) . 1 by ;
then (SgmX ((),sc)) /. 1 in rng (SgmX ((),sc)) by ;
then (SgmX ((),sc)) /. 1 = EmptyBag n by
.= (SgmX ((),sc)) /. u by ;
hence contradiction by A7, A15, A18, A22, PRE_POLY:def 2; :: thesis: verum
end;
for u being object st u in {1} holds
u in dom (SgmX ((),sc)) by ;
then A24: dom (SgmX ((),sc)) = Seg 1 by ;
then A25: 1 in dom (SgmX ((),sc)) by ;
(SgmX ((),sc)) /. 1 = (SgmX ((),sc)) . 1 by ;
then (SgmX ((),sc)) /. 1 in rng (SgmX ((),sc)) by ;
then A26: (SgmX ((),sc)) /. 1 = EmptyBag n by ;
A27: len (SgmX ((),sc)) = 1 by ;
dom c = Bags n by FUNCT_2:def 1;
then 1 in dom (c * (SgmX ((),sc))) by ;
then A28: (c * (SgmX ((),sc))) /. 1 = (c * (SgmX ((),sc))) . 1 by PARTFUN1:def 6
.= c . ((SgmX ((),sc)) . 1) by
.= c . () by
.= coefficient c by Lm2 ;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX ((),sc)) by ;
then y . 1 = y /. 1 by
.= () * (eval ((),x)) by A1, A3, A27, A26, A28
.= () * (1. L) by POLYNOM2:14
.= coefficient c ;
then y = <*()*> by ;
hence eval (c,x) = coefficient c by ; :: thesis: verum
end;
end;
end;
hence eval (c,x) = coefficient c ; :: thesis: verum