let n be Ordinal; :: thesis: for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative commutative 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 well-unital distributive associative commutative 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 ((),(Support (p * a)))) and
A2: eval ((p * a),x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = (((p * a) * (SgmX ((),(Support (p * a))))) /. i) * (eval (((SgmX ((),(Support (p * a)))) /. i),x)) by POLYNOM2:def 4;
consider z being FinSequence of the carrier of L such that
A4: len z = len (SgmX ((),())) and
A5: eval (p,x) = Sum z and
A6: for i being Element of NAT st 1 <= i & i <= len z holds
z /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) by POLYNOM2:def 4;
now :: thesis: ( ( a = 0. L & eval ((p * a),x) = (eval (p,x)) * a ) or ( a <> 0. L & eval ((p * a),x) = (eval (p,x)) * a ) )
per cases ( a = 0. L or a <> 0. L ) ;
case A7: a = 0. L ; :: thesis: eval ((p * a),x) = (eval (p,x)) * a
A8: now :: thesis: for b being bag of n holds (p * a) . b = 0. L
let b be bag of n; :: thesis: (p * a) . b = 0. L
thus (p * a) . b = (p . b) * a by Def10
.= 0. L by A7 ; :: thesis: verum
end;
A9: now :: thesis: not Support (p * a) <> {}
assume Support (p * a) <> {} ; :: thesis: contradiction
then reconsider sp = Support (p * a) as non empty Subset of (Bags n) ;
set c = the Element of sp;
(p * a) . the Element of sp <> 0. L by POLYNOM1:def 4;
hence contradiction by A8; :: thesis: verum
end;
BagOrder n linearly_orders Support (p * a) by POLYNOM2:18;
then rng (SgmX ((),(Support (p * a)))) = {} by ;
then SgmX ((),(Support (p * a))) = {} by RELAT_1:41;
then y = <*> the carrier of L by A1;
then Sum y = 0. L by RLVECT_1:43
.= (Sum z) * a by A7 ;
hence eval ((p * a),x) = (eval (p,x)) * a by A2, A5; :: thesis: verum
end;
case A10: a <> 0. L ; :: thesis: eval ((p * a),x) = (eval (p,x)) * a
A11: for u being object st u in Support (p * a) holds
u in Support p
proof
let u be object ; :: thesis: ( u in Support (p * a) implies u in Support p )
assume A12: u in Support (p * a) ; :: thesis:
then reconsider u9 = u as Element of Bags n ;
(p * a) . u <> 0. L by ;
then (p . u9) * a <> 0. L by Def10;
then p . u9 <> 0. L ;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum
end;
A13: for u being object st u in Support p holds
u in Support (p * a)
proof
let u be object ; :: thesis: ( u in Support p implies u in Support (p * a) )
assume A14: u in Support p ; :: thesis: u in Support (p * a)
then reconsider u9 = u as Element of Bags n ;
p . u <> 0. L by ;
then (p . u9) * a <> 0. L by ;
then (p * a) . u9 <> 0. L by Def10;
hence u in Support (p * a) by POLYNOM1:def 4; :: thesis: verum
end;
then A15: len z = len y by ;
then A16: dom z = Seg (len y) by FINSEQ_1:def 3
.= dom y by FINSEQ_1:def 3 ;
A17: BagOrder n linearly_orders Support (p * a) by POLYNOM2:18;
A18: Support (p * a) = Support p by ;
now :: thesis: for i being object st i in dom z holds
y /. i = (z /. i) * a
A19: dom (p * a) = Bags n by FUNCT_2:def 1;
now :: thesis: for u being object st u in rng (SgmX ((),(Support (p * a)))) holds
u in dom (p * a)
let u be object ; :: thesis: ( u in rng (SgmX ((),(Support (p * a)))) implies u in dom (p * a) )
assume u in rng (SgmX ((),(Support (p * a)))) ; :: thesis: u in dom (p * a)
then u in Support (p * a) by ;
hence u in dom (p * a) by A19; :: thesis: verum
end;
then rng (SgmX ((),(Support (p * a)))) c= dom (p * a) by TARSKI:def 3;
then reconsider r = (p * a) * (SgmX ((),(Support (p * a)))) as FinSequence by FINSEQ_1:16;
for u being object st u in rng r holds
u in the carrier of L
proof
let u be object ; :: 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 A20: u in rng (p * a) by FUNCT_1:14;
rng (p * a) c= the carrier of L by RELAT_1:def 19;
hence u in the carrier of L by A20; :: thesis: verum
end;
then A21: rng r c= the carrier of L by TARSKI:def 3;
A22: dom p = Bags n by FUNCT_2:def 1;
now :: thesis: for u being object st u in rng (SgmX ((),(Support (p * a)))) holds
u in dom p
let u be object ; :: thesis: ( u in rng (SgmX ((),(Support (p * a)))) implies u in dom p )
assume u in rng (SgmX ((),(Support (p * a)))) ; :: thesis: u in dom p
then u in Support (p * a) by ;
hence u in dom p by A22; :: thesis: verum
end;
then rng (SgmX ((),(Support (p * a)))) c= dom p by TARSKI:def 3;
then reconsider q = p * (SgmX ((),(Support (p * a)))) as FinSequence by FINSEQ_1:16;
for u being object st u in rng q holds
u in the carrier of L
proof
let u be object ; :: 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 A23: u in rng p by FUNCT_1:14;
rng p c= the carrier of L by RELAT_1:def 19;
hence u in the carrier of L by A23; :: thesis: verum
end;
then A24: rng q c= the carrier of L by TARSKI:def 3;
reconsider r = r as FinSequence of the carrier of L by ;
reconsider q = q as FinSequence of the carrier of L by ;
let i be object ; :: thesis: ( i in dom z implies y /. i = (z /. i) * a )
assume A25: 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 Nat : ( 1 <= k & k <= len z ) } by FINSEQ_1:def 1;
then consider k being Nat such that
A26: i = k and
A27: ( 1 <= k & k <= len z ) ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A28: dom z = Seg (len (SgmX ((),(Support (p * a))))) by
.= dom (SgmX ((),(Support (p * a)))) by FINSEQ_1:def 3 ;
then (SgmX ((),(Support (p * a)))) . k = (SgmX ((),(Support (p * a)))) /. k by ;
then k in dom q by ;
then A29: (p * (SgmX ((),(Support (p * a))))) /. k = q . k by PARTFUN1:def 6
.= p . ((SgmX ((),(Support (p * a)))) . k) by
.= p . ((SgmX ((),(Support (p * a)))) /. k) by ;
reconsider c = (SgmX ((),(Support (p * a)))) /. k as Element of Bags n ;
reconsider c = c as bag of n ;
A30: (z /. k) * a = (((p * (SgmX ((),(Support (p * a))))) /. k) * (eval (((SgmX ((),(Support (p * a)))) /. k),x))) * a by A6, A18, A27
.= (((p * (SgmX ((),(Support (p * a))))) /. k) * a) * (eval (((SgmX ((),(Support (p * a)))) /. k),x)) by GROUP_1:def 3 ;
A31: (p * a) . ((SgmX ((),(Support (p * a)))) /. k) = ((p * (SgmX ((),(Support (p * a))))) /. k) * a by ;
(SgmX ((),(Support (p * a)))) . k = (SgmX ((),(Support (p * a)))) /. k by ;
then k in dom r by ;
then ((p * a) * (SgmX ((),(Support (p * a))))) /. k = r . k by PARTFUN1:def 6
.= (p * a) . ((SgmX ((),(Support (p * a)))) . k) by
.= ((p * (SgmX ((),(Support (p * a))))) /. k) * a by ;
hence y /. i = (z /. i) * a by A3, A15, A26, A27, A30; :: thesis: verum
end;
then y = z * a by ;
hence eval ((p * a),x) = (eval (p,x)) * a by ; :: thesis: verum
end;
end;
end;
hence eval ((p * a),x) = (eval (p,x)) * a ; :: thesis: verum