let n be Ordinal; :: thesis: for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative well-unital distributive domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (a * p),x = a * (eval p,x)
let L be non trivial left_add-cancelable right_complementable add-associative right_zeroed associative well-unital distributive domRing-like left_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (a * p),x = a * (eval p,x)
let p be Polynomial of n,L; :: thesis: for a being Element of L
for x being Function of n,L holds eval (a * p),x = a * (eval p,x)
let a be Element of L; :: thesis: for x being Function of n,L holds eval (a * p),x = a * (eval p,x)
let x be Function of n,L; :: thesis: eval (a * p),x = a * (eval p,x)
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX (BagOrder n),(Support (a * p))) and
A2: eval (a * p),x = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((a * p) * (SgmX (BagOrder n),(Support (a * p)))) /. i) * (eval (((SgmX (BagOrder n),(Support (a * p))) /. i) @ ),x) by POLYNOM2:def 4;
A4: BagOrder n linearly_orders Support (a * p) by POLYNOM2:20;
consider z being FinSequence of the carrier of L such that
A5: len z = len (SgmX (BagOrder n),(Support p)) and
A6: eval p,x = Sum z and
A7: for i being Element of NAT st 1 <= i & i <= len z holds
z /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) by POLYNOM2:def 4;

per cases ( a = 0. L or a <> 0. L ) ;

suppose A8: a = 0. L ; :: thesis: eval (a * p),x = a * (eval p,x)

A9: now

let b be bag of n; :: thesis: (a * p) . b = 0. L
thus (a * p) . b = a * (p . b) by Def10
.= 0. L by A8, BINOM:1 ; :: thesis: verum

end;

now

assume Support (a * p) <> {} ; :: thesis: contradiction
then reconsider sp = Support (a * p) as non empty Subset of (Bags n) ;
consider c being Element of sp;
(a * p) . c <> 0. L by POLYNOM1:def 9;
hence contradiction by A9; :: thesis: verum

end;

then rng (SgmX (BagOrder n),(Support (a * p))) = {} by A4, PRE_POLY:def 2;
then SgmX (BagOrder n),(Support (a * p)) = {} by RELAT_1:64;
then y = <*> the carrier of L by A1;
then Sum y = 0. L by RLVECT_1:60
.= a * (Sum z) by A8, BINOM:1 ;
hence eval (a * p),x = a * (eval p,x) by A2, A6; :: thesis: verum

end;

suppose A10: a <> 0. L ; :: thesis: eval (a * p),x = a * (eval p,x)

A11: for u being set st u in Support (a * p) holds
u in Support p

proof

let u be set ; :: thesis: ( u in Support (a * p) implies u in Support p )
assume A12: u in Support (a * p) ; :: thesis: u in Support p
then reconsider u9 = u as Element of Bags n ;
(a * p) . u <> 0. L by A12, POLYNOM1:def 9;
then a * (p . u9) <> 0. L by Def10;
then p . u9 <> 0. L by BINOM:2;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

A13: for u being set st u in Support p holds
u in Support (a * p)

proof

let u be set ; :: thesis: ( u in Support p implies u in Support (a * p) )
assume A14: u in Support p ; :: thesis: u in Support (a * p)
then reconsider u9 = u as Element of Bags n ;
p . u <> 0. L by A14, POLYNOM1:def 9;
then a * (p . u9) <> 0. L by A10, VECTSP_2:def 5;
then (a * p) . u9 <> 0. L by Def10;
hence u in Support (a * p) by POLYNOM1:def 9; :: thesis: verum

end;

then A15: len z = len y by A1, A5, A11, TARSKI:2;
then A16: dom z = Seg (len y) by FINSEQ_1:def 3
.= dom y by FINSEQ_1:def 3 ;
A17: Support (a * p) = Support p by A13, A11, TARSKI:2;

now

A18: dom (a * p) = Bags n by FUNCT_2:def 1;

now

let u be set ; :: thesis: ( u in rng (SgmX (BagOrder n),(Support (a * p))) implies u in dom (a * p) )
assume u in rng (SgmX (BagOrder n),(Support (a * p))) ; :: thesis: u in dom (a * p)
then u in Support (a * p) by A4, PRE_POLY:def 2;
hence u in dom (a * p) by A18; :: thesis: verum

end;

then rng (SgmX (BagOrder n),(Support (a * p))) c= dom (a * p) by TARSKI:def 3;
then reconsider r = (a * p) * (SgmX (BagOrder n),(Support (a * p))) as FinSequence by FINSEQ_1:20;
for u being set st u in rng r holds
u in the carrier of L

proof

let u be set ; :: thesis: ( u in rng r implies u in the carrier of L )
assume u in rng r ; :: thesis: u in the carrier of L
then A19: u in rng (a * p) by FUNCT_1:25;
rng (a * p) c= the carrier of L by RELAT_1:def 19;
hence u in the carrier of L by A19; :: thesis: verum

end;

then A20: rng r c= the carrier of L by TARSKI:def 3;
A21: dom p = Bags n by FUNCT_2:def 1;

now

let u be set ; :: thesis: ( u in rng (SgmX (BagOrder n),(Support (a * p))) implies u in dom p )
assume u in rng (SgmX (BagOrder n),(Support (a * p))) ; :: thesis: u in dom p
then u in Support (a * p) by A4, PRE_POLY:def 2;
hence u in dom p by A21; :: thesis: verum

end;

then rng (SgmX (BagOrder n),(Support (a * p))) c= dom p by TARSKI:def 3;
then reconsider q = p * (SgmX (BagOrder n),(Support (a * p))) as FinSequence by FINSEQ_1:20;
for u being set st u in rng q holds
u in the carrier of L

proof

let u be set ; :: thesis: ( u in rng q implies u in the carrier of L )
assume u in rng q ; :: thesis: u in the carrier of L
then A22: u in rng p by FUNCT_1:25;
rng p c= the carrier of L by RELAT_1:def 19;
hence u in the carrier of L by A22; :: thesis: verum

end;

then A23: rng q c= the carrier of L by TARSKI:def 3;
reconsider r = r as FinSequence of the carrier of L by A20, FINSEQ_1:def 4;
reconsider q = q as FinSequence of the carrier of L by A23, FINSEQ_1:def 4;
let i be set ; :: thesis: ( i in dom z implies y /. i = a * (z /. i) )
assume A24: i in dom z ; :: thesis: y /. i = a * (z /. i)
then i in Seg (len z) by FINSEQ_1:def 3;
then i in { k where k is Element of NAT : ( 1 <= k & k <= len z ) } by FINSEQ_1:def 1;
then consider k being Element of NAT such that
A25: i = k and
A26: ( 1 <= k & k <= len z ) ;
A27: dom z = Seg (len (SgmX (BagOrder n),(Support (a * p)))) by A1, A16, FINSEQ_1:def 3
.= dom (SgmX (BagOrder n),(Support (a * p))) by FINSEQ_1:def 3 ;
then (SgmX (BagOrder n),(Support (a * p))) . k = (SgmX (BagOrder n),(Support (a * p))) /. k by A24, A25, PARTFUN1:def 8;
then k in dom q by A24, A25, A27, A21, FUNCT_1:21;
then A28: (p * (SgmX (BagOrder n),(Support (a * p)))) /. k = q . k by PARTFUN1:def 8
.= p . ((SgmX (BagOrder n),(Support (a * p))) . k) by A24, A25, A27, FUNCT_1:23
.= p . ((SgmX (BagOrder n),(Support (a * p))) /. k) by A24, A25, A27, PARTFUN1:def 8 ;
reconsider c = (SgmX (BagOrder n),(Support (a * p))) /. k as Element of Bags n ;
reconsider c = c as bag of n ;
A29: a * (z /. k) = a * (((p * (SgmX (BagOrder n),(Support p))) /. k) * (eval (((SgmX (BagOrder n),(Support p)) /. k) @ ),x)) by A7, A26
.= (a * ((p * (SgmX (BagOrder n),(Support (a * p)))) /. k)) * (eval (((SgmX (BagOrder n),(Support (a * p))) /. k) @ ),x) by A17, GROUP_1:def 4 ;
A30: (a * p) . ((SgmX (BagOrder n),(Support (a * p))) /. k) = (a * p) . c
.= a * ((p * (SgmX (BagOrder n),(Support (a * p)))) /. k) by A28, Def10 ;
(SgmX (BagOrder n),(Support (a * p))) . k = (SgmX (BagOrder n),(Support (a * p))) /. k by A24, A25, A27, PARTFUN1:def 8;
then k in dom r by A24, A25, A27, A18, FUNCT_1:21;
then ((a * p) * (SgmX (BagOrder n),(Support (a * p)))) /. k = r . k by PARTFUN1:def 8
.= (a * p) . ((SgmX (BagOrder n),(Support (a * p))) . k) by A24, A25, A27, FUNCT_1:23
.= a * ((p * (SgmX (BagOrder n),(Support (a * p)))) /. k) by A24, A25, A27, A30, PARTFUN1:def 8 ;
hence y /. i = a * (z /. i) by A3, A15, A25, A26, A29; :: thesis: verum

end;

then y = a * z by A16, POLYNOM1:def 2;
hence eval (a * p),x = a * (eval p,x) by A2, A6, BINOM:4; :: thesis: verum

end;

end;