let n be Ordinal; :: thesis: for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed associative commutative 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 (p * a),x = (eval p,x) * a
let L be non trivial left_add-cancelable right_complementable add-associative right_zeroed associative commutative 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 (p * a),x = (eval p,x) * a
let p be Polynomial of n,L; :: thesis: for a being Element of L
for x being Function of n,L holds eval (p * a),x = (eval p,x) * a
let a be Element of L; :: thesis: for x being Function of n,L holds eval (p * a),x = (eval p,x) * a
let x be Function of n,L; :: thesis: eval (p * a),x = (eval p,x) * a
consider y being FinSequence of the carrier of L such that
A1: ( len y = len (SgmX (BagOrder n),(Support (p * a))) & eval (p * a),x = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((p * a) * (SgmX (BagOrder n),(Support (p * a)))) /. i) * (eval (((SgmX (BagOrder n),(Support (p * a))) /. i) @ ),x) ) ) by POLYNOM2:def 4;
consider z being FinSequence of the carrier of L such that
A2: ( len z = len (SgmX (BagOrder n),(Support p)) & eval p,x = Sum z & ( 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;

now

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

case A3: a = 0. L ; :: thesis: eval (p * a),x = (eval p,x) * a

A4: now

let b be bag of ; :: thesis: (p * a) . b = 0. L
thus (p * a) . b = (p . b) * a by Def11
.= 0. L by A3, BINOM:2 ; :: thesis: verum

end;

A5: now

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

end;

BagOrder n linearly_orders Support (p * a) by POLYNOM2:20;
then rng (SgmX (BagOrder n),(Support (p * a))) = {} by A5, TRIANG_1:def 2;
then SgmX (BagOrder n),(Support (p * a)) = {} by RELAT_1:64;
then len y = 0 by A1;
then y = <*> the carrier of L ;
then Sum y = 0. L by RLVECT_1:60
.= (Sum z) * a by A3, BINOM:2 ;
hence eval (p * a),x = (eval p,x) * a by A1, A2; :: thesis: verum

end;

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

A7: BagOrder n linearly_orders Support (p * a) by POLYNOM2:20;
A8: for u being set st u in Support p holds
u in Support (p * a)

proof

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

end;

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

proof

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

end;

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

now

let i be set ; :: thesis: ( i in dom z implies y /. i = (z /. i) * a )
assume A16: i in dom z ; :: thesis: y /. i = (z /. i) * a
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
A17: ( i = k & 1 <= k & k <= len z ) ;
A18: (z /. k) * a = (((p * (SgmX (BagOrder n),(Support (p * a)))) /. k) * (eval (((SgmX (BagOrder n),(Support (p * a))) /. k) @ ),x)) * a by A2, A13, A17
.= (((p * (SgmX (BagOrder n),(Support (p * a)))) /. k) * a) * (eval (((SgmX (BagOrder n),(Support (p * a))) /. k) @ ),x) by GROUP_1:def 4 ;
A19: dom z = Seg (len (SgmX (BagOrder n),(Support (p * a)))) by A1, A15, FINSEQ_1:def 3
.= dom (SgmX (BagOrder n),(Support (p * a))) by FINSEQ_1:def 3 ;
A20: dom p = Bags n by FUNCT_2:def 1;

now

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

end;

then rng (SgmX (BagOrder n),(Support (p * a))) c= dom p by TARSKI:def 3;
then reconsider q = p * (SgmX (BagOrder n),(Support (p * a))) 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 A21: 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 A21; :: thesis: verum

end;

then rng q c= the carrier of L by TARSKI:def 3;
then reconsider q = q as FinSequence of the carrier of L by FINSEQ_1:def 4;
(SgmX (BagOrder n),(Support (p * a))) . k = (SgmX (BagOrder n),(Support (p * a))) /. k by A16, A17, A19, PARTFUN1:def 8;
then k in dom q by A16, A17, A19, A20, FUNCT_1:21;
then A22: (p * (SgmX (BagOrder n),(Support (p * a)))) /. k = q . k by PARTFUN1:def 8
.= p . ((SgmX (BagOrder n),(Support (p * a))) . k) by A16, A17, A19, FUNCT_1:23
.= p . ((SgmX (BagOrder n),(Support (p * a))) /. k) by A16, A17, A19, PARTFUN1:def 8 ;
reconsider c = (SgmX (BagOrder n),(Support (p * a))) /. k as Element of Bags n ;
reconsider c = c as bag of ;
A23: (p * a) . ((SgmX (BagOrder n),(Support (p * a))) /. k) = (p * a) . c
.= ((p * (SgmX (BagOrder n),(Support (p * a)))) /. k) * a by A22, Def11 ;
A24: dom (p * a) = Bags n by FUNCT_2:def 1;

now

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

end;

then rng (SgmX (BagOrder n),(Support (p * a))) c= dom (p * a) by TARSKI:def 3;
then reconsider r = (p * a) * (SgmX (BagOrder n),(Support (p * a))) 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 A25: u in rng (p * a) by FUNCT_1:25;
rng (p * a) c= the carrier of L by RELAT_1:def 19;
hence u in the carrier of L by A25; :: thesis: verum

end;

then rng r c= the carrier of L by TARSKI:def 3;
then reconsider r = r as FinSequence of the carrier of L by FINSEQ_1:def 4;
(SgmX (BagOrder n),(Support (p * a))) . k = (SgmX (BagOrder n),(Support (p * a))) /. k by A16, A17, A19, PARTFUN1:def 8;
then k in dom r by A16, A17, A19, A24, FUNCT_1:21;
then ((p * a) * (SgmX (BagOrder n),(Support (p * a)))) /. k = r . k by PARTFUN1:def 8
.= (p * a) . ((SgmX (BagOrder n),(Support (p * a))) . k) by A16, A17, A19, FUNCT_1:23
.= ((p * (SgmX (BagOrder n),(Support (p * a)))) /. k) * a by A16, A17, A19, A23, PARTFUN1:def 8 ;
hence y /. i = (z /. i) * a by A1, A14, A17, A18; :: thesis: verum

end;

then y = z * a by A15, POLYNOM1:def 3;
hence eval (p * a),x = (eval p,x) * a by A1, A2, BINOM:5; :: thesis: verum

end;

end;

end;

hence eval (p * a),x = (eval p,x) * a ; :: thesis: verum