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 ((BagOrder n),(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 ((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

A4: len z = len (SgmX ((BagOrder n),(Support p))) 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 ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by POLYNOM2:def 4;

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 ((BagOrder n),(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 ((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

A4: len z = len (SgmX ((BagOrder n),(Support p))) 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 ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. 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 ) )end;

hence
eval ((p * a),x) = (eval (p,x)) * a
; :: thesis: verumper cases
( a = 0. L or a <> 0. L )
;

end;

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

then rng (SgmX ((BagOrder n),(Support (p * a)))) = {} by A9, PRE_POLY:def 2;

then SgmX ((BagOrder n),(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;

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;thus (p * a) . b = (p . b) * a by Def10

.= 0. L by A7 ; :: thesis: verum

A9: now :: thesis: not Support (p * a) <> {}

BagOrder n linearly_orders Support (p * a)
by POLYNOM2:18;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;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

then rng (SgmX ((BagOrder n),(Support (p * a)))) = {} by A9, PRE_POLY:def 2;

then SgmX ((BagOrder n),(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

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

u in Support (p * a)

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 A13, A11, TARSKI:2;

hence eval ((p * a),x) = (eval (p,x)) * a by A2, A5, BINOM:5; :: thesis: verum

end;u in Support p

proof

A13:
for u being object st u in Support p holds
let u be object ; :: 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 u9 = u as Element of Bags n ;

(p * a) . u <> 0. L by A12, POLYNOM1:def 4;

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;assume A12: u in Support (p * a) ; :: thesis: u in Support p

then reconsider u9 = u as Element of Bags n ;

(p * a) . u <> 0. L by A12, POLYNOM1:def 4;

then (p . u9) * a <> 0. L by Def10;

then p . u9 <> 0. L ;

hence u in Support p by POLYNOM1:def 4; :: thesis: verum

u in Support (p * a)

proof

then A15:
len z = len y
by A1, A4, A11, TARSKI:2;
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 A14, POLYNOM1:def 4;

then (p . u9) * a <> 0. L by A10, VECTSP_2:def 1;

then (p * a) . u9 <> 0. L by Def10;

hence u in Support (p * a) by POLYNOM1:def 4; :: thesis: verum

end;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 A14, POLYNOM1:def 4;

then (p . u9) * a <> 0. L by A10, VECTSP_2:def 1;

then (p * a) . u9 <> 0. L by Def10;

hence u in Support (p * a) by POLYNOM1:def 4; :: thesis: verum

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 A13, A11, TARSKI:2;

now :: thesis: for i being object st i in dom z holds

y /. i = (z /. i) * a

then
y = z * a
by A16, POLYNOM1:def 2;y /. i = (z /. i) * a

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

then reconsider r = (p * a) * (SgmX ((BagOrder n),(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

A22: dom p = Bags n by FUNCT_2:def 1;

then reconsider q = p * (SgmX ((BagOrder n),(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

reconsider r = r as FinSequence of the carrier of L by A21, FINSEQ_1:def 4;

reconsider q = q as FinSequence of the carrier of L by A24, FINSEQ_1:def 4;

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 ((BagOrder n),(Support (p * a))))) by A1, A16, FINSEQ_1:def 3

.= dom (SgmX ((BagOrder n),(Support (p * a)))) by FINSEQ_1:def 3 ;

then (SgmX ((BagOrder n),(Support (p * a)))) . k = (SgmX ((BagOrder n),(Support (p * a)))) /. k by A25, A26, PARTFUN1:def 6;

then k in dom q by A25, A26, A28, A22, FUNCT_1:11;

then A29: (p * (SgmX ((BagOrder n),(Support (p * a))))) /. k = q . k by PARTFUN1:def 6

.= p . ((SgmX ((BagOrder n),(Support (p * a)))) . k) by A25, A26, A28, FUNCT_1:13

.= p . ((SgmX ((BagOrder n),(Support (p * a)))) /. k) by A25, A26, A28, PARTFUN1:def 6 ;

reconsider c = (SgmX ((BagOrder n),(Support (p * a)))) /. k as Element of Bags n ;

reconsider c = c as bag of n ;

A30: (z /. k) * a = (((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * (eval (((SgmX ((BagOrder n),(Support (p * a)))) /. k),x))) * a by A6, A18, A27

.= (((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a) * (eval (((SgmX ((BagOrder n),(Support (p * a)))) /. k),x)) by GROUP_1:def 3 ;

A31: (p * a) . ((SgmX ((BagOrder n),(Support (p * a)))) /. k) = ((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a by A29, Def10;

(SgmX ((BagOrder n),(Support (p * a)))) . k = (SgmX ((BagOrder n),(Support (p * a)))) /. k by A25, A26, A28, PARTFUN1:def 6;

then k in dom r by A25, A26, A28, A19, FUNCT_1:11;

then ((p * a) * (SgmX ((BagOrder n),(Support (p * a))))) /. k = r . k by PARTFUN1:def 6

.= (p * a) . ((SgmX ((BagOrder n),(Support (p * a)))) . k) by A25, A26, A28, FUNCT_1:13

.= ((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a by A25, A26, A28, A31, PARTFUN1:def 6 ;

hence y /. i = (z /. i) * a by A3, A15, A26, A27, A30; :: thesis: verum

end;now :: thesis: for u being object st u in rng (SgmX ((BagOrder n),(Support (p * a)))) holds

u in dom (p * a)

then
rng (SgmX ((BagOrder n),(Support (p * a)))) c= dom (p * a)
by TARSKI:def 3;u in dom (p * a)

let u be object ; :: 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 A17, PRE_POLY:def 2;

hence u in dom (p * a) by A19; :: thesis: verum

end;assume u in rng (SgmX ((BagOrder n),(Support (p * a)))) ; :: thesis: u in dom (p * a)

then u in Support (p * a) by A17, PRE_POLY:def 2;

hence u in dom (p * a) by A19; :: thesis: verum

then reconsider r = (p * a) * (SgmX ((BagOrder n),(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

then A21:
rng r c= the carrier of L
by TARSKI:def 3;
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;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

A22: dom p = Bags n by FUNCT_2:def 1;

now :: thesis: for u being object st u in rng (SgmX ((BagOrder n),(Support (p * a)))) holds

u in dom p

then
rng (SgmX ((BagOrder n),(Support (p * a)))) c= dom p
by TARSKI:def 3;u in dom p

let u be object ; :: 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 A17, PRE_POLY:def 2;

hence u in dom p by A22; :: thesis: verum

end;assume u in rng (SgmX ((BagOrder n),(Support (p * a)))) ; :: thesis: u in dom p

then u in Support (p * a) by A17, PRE_POLY:def 2;

hence u in dom p by A22; :: thesis: verum

then reconsider q = p * (SgmX ((BagOrder n),(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

then A24:
rng q c= the carrier of L
by TARSKI:def 3;
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;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

reconsider r = r as FinSequence of the carrier of L by A21, FINSEQ_1:def 4;

reconsider q = q as FinSequence of the carrier of L by A24, FINSEQ_1:def 4;

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 ((BagOrder n),(Support (p * a))))) by A1, A16, FINSEQ_1:def 3

.= dom (SgmX ((BagOrder n),(Support (p * a)))) by FINSEQ_1:def 3 ;

then (SgmX ((BagOrder n),(Support (p * a)))) . k = (SgmX ((BagOrder n),(Support (p * a)))) /. k by A25, A26, PARTFUN1:def 6;

then k in dom q by A25, A26, A28, A22, FUNCT_1:11;

then A29: (p * (SgmX ((BagOrder n),(Support (p * a))))) /. k = q . k by PARTFUN1:def 6

.= p . ((SgmX ((BagOrder n),(Support (p * a)))) . k) by A25, A26, A28, FUNCT_1:13

.= p . ((SgmX ((BagOrder n),(Support (p * a)))) /. k) by A25, A26, A28, PARTFUN1:def 6 ;

reconsider c = (SgmX ((BagOrder n),(Support (p * a)))) /. k as Element of Bags n ;

reconsider c = c as bag of n ;

A30: (z /. k) * a = (((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * (eval (((SgmX ((BagOrder n),(Support (p * a)))) /. k),x))) * a by A6, A18, A27

.= (((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a) * (eval (((SgmX ((BagOrder n),(Support (p * a)))) /. k),x)) by GROUP_1:def 3 ;

A31: (p * a) . ((SgmX ((BagOrder n),(Support (p * a)))) /. k) = ((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a by A29, Def10;

(SgmX ((BagOrder n),(Support (p * a)))) . k = (SgmX ((BagOrder n),(Support (p * a)))) /. k by A25, A26, A28, PARTFUN1:def 6;

then k in dom r by A25, A26, A28, A19, FUNCT_1:11;

then ((p * a) * (SgmX ((BagOrder n),(Support (p * a))))) /. k = r . k by PARTFUN1:def 6

.= (p * a) . ((SgmX ((BagOrder n),(Support (p * a)))) . k) by A25, A26, A28, FUNCT_1:13

.= ((p * (SgmX ((BagOrder n),(Support (p * a))))) /. k) * a by A25, A26, A28, A31, PARTFUN1:def 6 ;

hence y /. i = (z /. i) * a by A3, A15, A26, A27, A30; :: thesis: verum

hence eval ((p * a),x) = (eval (p,x)) * a by A2, A5, BINOM:5; :: thesis: verum