let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for q being Polynomial of n,L st ex b being bag of st Support q = {b} holds
for p being Polynomial of n,L
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for q being Polynomial of n,L st ex b being bag of st Support q = {b} holds
for p being Polynomial of n,L
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let q be Polynomial of n,L; :: thesis: ( ex b being bag of st Support q = {b} implies for p being Polynomial of n,L
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x) )
given b being bag of such that A1: Support q = {b} ; :: thesis: for p being Polynomial of n,L
for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let p be Polynomial of n,L; :: thesis: for x being Function of n,L holds eval (p *' q),x = (eval p,x) * (eval q,x)
let x be Function of n,L; :: thesis: eval (p *' q),x = (eval p,x) * (eval q,x)
defpred S₁[ Element of NAT ] means for p being Polynomial of n,L st card (Support p) = $1 holds
eval (p *' q),x = (eval p,x) * (eval q,x);
A2: S₁[ 0 ]

proof

let p be Polynomial of n,L; :: thesis: ( card (Support p) = 0 implies eval (p *' q),x = (eval p,x) * (eval q,x) )
assume card (Support p) = 0 ; :: thesis: eval (p *' q),x = (eval p,x) * (eval q,x)
then Support p = {} ;
then A3: p = 0_ n,L by Th19;
hence eval (p *' q),x = eval p,x by POLYNOM1:87
.= 0. L by A3, Th22
.= (0. L) * (eval q,x) by VECTSP_1:39
.= (eval p,x) * (eval q,x) by A3, Th22 ;
:: thesis: verum

end;

A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let p be Polynomial of n,L; :: thesis: ( card (Support p) = k + 1 implies eval (p *' q),x = (eval p,x) * (eval q,x) )
assume A6: card (Support p) = k + 1 ; :: thesis: eval (p *' q),x = (eval p,x) * (eval q,x)
set sgp = SgmX (BagOrder n),(Support p);
set bg = (SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)));
set p' = p +* ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))),(0. L);
set m = (0_ n,L) +* ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))),(p . ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))));
A7: BagOrder n linearly_orders Support p by Th20;
then rng (SgmX (BagOrder n),(Support p)) <> {} by A6, CARD_1:47, TRIANG_1:def 2;
then SgmX (BagOrder n),(Support p) <> {} by RELAT_1:60;
then len (SgmX (BagOrder n),(Support p)) <> 0 ;
then 1 <= len (SgmX (BagOrder n),(Support p)) by NAT_1:14;
then len (SgmX (BagOrder n),(Support p)) in Seg (len (SgmX (BagOrder n),(Support p))) by FINSEQ_1:3;
then A8: len (SgmX (BagOrder n),(Support p)) in dom (SgmX (BagOrder n),(Support p)) by FINSEQ_1:def 3;
then (SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))) = (SgmX (BagOrder n),(Support p)) . (len (SgmX (BagOrder n),(Support p))) by PARTFUN1:def 8;
then (SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))) in rng (SgmX (BagOrder n),(Support p)) by A8, FUNCT_1:def 5;
then A9: (SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))) in Support p by A7, TRIANG_1:def 2;
then A10: p . ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))) <> 0. L by POLYNOM1:def 9;
reconsider bg = (SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))) as bag of by POLYNOM1:def 14;
dom p = Bags n by FUNCT_2:def 1;
then A11: p +* ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))),(0. L) = p +* (bg .--> (0. L)) by FUNCT_7:def 3;
reconsider p' = p +* ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))),(0. L) as Function of (Bags n),the carrier of L ;
reconsider p' = p' as Function of (Bags n),L ;
for u being set st u in Support p' holds
u in Support p

proof

let u be set ; :: thesis: ( u in Support p' implies u in Support p )
assume A12: u in Support p' ; :: thesis: u in Support p
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of ;

now

assume A13: u = bg ; :: thesis: contradiction
then u in {bg} by TARSKI:def 1;
then u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then p' . u = (bg .--> (0. L)) . bg by A11, A13, FUNCT_4:14;
then p' . u = 0. L by FUNCOP_1:87;
hence contradiction by A12, POLYNOM1:def 9; :: thesis: verum

end;

then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then p . u = p' . u by A11, FUNCT_4:12;
then p . u <> 0. L by A12, POLYNOM1:def 9;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

then Support p' c= Support p by TARSKI:def 3;
then Support p' is finite ;
then reconsider p' = p' as Polynomial of n,L by POLYNOM1:def 10;
dom (0_ n,L) = Bags n by FUNCT_2:def 1;
then A14: (0_ n,L) +* ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))),(p . ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))))) = (0_ n,L) +* (bg .--> (p . bg)) by FUNCT_7:def 3;
reconsider m = (0_ n,L) +* ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p)))),(p . ((SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))))) as Function of (Bags n),the carrier of L ;
reconsider m = m as Function of (Bags n),L ;
A15: for u being set st u in Support m holds
u in {bg}

proof

let u be set ; :: thesis: ( u in Support m implies u in {bg} )
assume A16: u in Support m ; :: thesis: u in {bg}
then reconsider u = u as Element of Bags n ;
A17: m . u <> 0. L by A16, POLYNOM1:def 9;

now

assume u <> bg ; :: thesis: contradiction
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (p . bg)) by FUNCOP_1:19;
then m . u = (0_ n,L) . u by A14, FUNCT_4:12;
hence contradiction by A17, POLYNOM1:81; :: thesis: verum

end;

hence u in {bg} by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {bg} holds
u in Support m

proof

let u be set ; :: thesis: ( u in {bg} implies u in Support m )
assume u in {bg} ; :: thesis: u in Support m
then A18: u = bg by TARSKI:def 1;
bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) by FUNCOP_1:19;
then m . bg = (bg .--> (p . bg)) . bg by A14, FUNCT_4:14;
then m . bg = p . bg by FUNCOP_1:87;
hence u in Support m by A10, A18, POLYNOM1:def 9; :: thesis: verum

end;

then A19: Support m = {bg} by A15, TARSKI:2;
then reconsider m = m as Polynomial of n,L by POLYNOM1:def 10;
reconsider m = m as Polynomial of n,L ;
bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (0. L)) by FUNCOP_1:19;
then p' . bg = (bg .--> (0. L)) . bg by A11, FUNCT_4:14;
then A20: p' . bg = 0. L by FUNCOP_1:87;
then A21: not bg in Support p' by POLYNOM1:def 9;
A22: for u being set st u in Support p holds
u in (Support p') \/ {bg}

proof

let u be set ; :: thesis: ( u in Support p implies u in (Support p') \/ {bg} )
assume A23: u in Support p ; :: thesis: u in (Support p') \/ {bg}
then reconsider u = u as Element of Bags n ;
A24: p . u <> 0. L by A23, POLYNOM1:def 9;

per cases ( u = bg or u <> bg ) ;

suppose u = bg ; :: thesis: u in (Support p') \/ {bg}

then u in {bg} by TARSKI:def 1;
hence u in (Support p') \/ {bg} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose u <> bg ; :: thesis: u in (Support p') \/ {bg}

then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then p' . u = p . u by A11, FUNCT_4:12;
then u in Support p' by A24, POLYNOM1:def 9;
hence u in (Support p') \/ {bg} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

for u being set st u in (Support p') \/ {bg} holds
u in Support p

proof

let u be set ; :: thesis: ( u in (Support p') \/ {bg} implies u in Support p )
assume A25: u in (Support p') \/ {bg} ; :: thesis: u in Support p

per cases ( u in Support p' or u in {bg} ) by A25, XBOOLE_0:def 3;

suppose A26: u in Support p' ; :: thesis: u in Support p

then reconsider u = u as Element of Bags n ;
A27: p' . u <> 0. L by A26, POLYNOM1:def 9;
u <> bg by A20, A26, POLYNOM1:def 9;
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then p' . u = p . u by A11, FUNCT_4:12;
hence u in Support p by A27, POLYNOM1:def 9; :: thesis: verum

end;

suppose u in {bg} ; :: thesis: u in Support p

hence u in Support p by A9, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then Support p = (Support p') \/ {bg} by A22, TARSKI:2;
then A28: k + 1 = (card (Support p')) + 1 by A6, A21, CARD_2:54;
A29: ( dom (p' + m) = Bags n & dom p = Bags n ) by FUNCT_2:def 1;
A30: for u being set st u in Bags n holds
(p' + m) . u = p . u

proof

let u be set ; :: thesis: ( u in Bags n implies (p' + m) . u = p . u )
assume u in Bags n ; :: thesis: (p' + m) . u = p . u
then reconsider u = u as bag of by POLYNOM1:def 14;

per cases ( u = bg or u <> bg ) ;

suppose A31: u = bg ; :: thesis: (p' + m) . u = p . u

then u in {bg} by TARSKI:def 1;
then u in dom (bg .--> (0. L)) by FUNCOP_1:19;
then A32: p' . u = (bg .--> (0. L)) . bg by A11, A31, FUNCT_4:14;
bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) by FUNCOP_1:19;
then m . bg = (bg .--> (p . bg)) . bg by A14, FUNCT_4:14;
then A33: m . bg = p . bg by FUNCOP_1:87;
(p' + m) . u = (p' . u) + (m . u) by POLYNOM1:def 21
.= (0. L) + (p . bg) by A31, A32, A33, FUNCOP_1:87
.= p . bg by RLVECT_1:def 7 ;
hence (p' + m) . u = p . u by A31; :: thesis: verum

end;

suppose u <> bg ; :: thesis: (p' + m) . u = p . u

then A34: not u in {bg} by TARSKI:def 1;
then A35: not u in dom (bg .--> (0. L)) by FUNCOP_1:19;
not u in dom (bg .--> (p . bg)) by A34, FUNCOP_1:19;
then m . u = (0_ n,L) . u by A14, FUNCT_4:12;
then A36: m . u = 0. L by POLYNOM1:81;
(p' + m) . u = (p' . u) + (m . u) by POLYNOM1:def 21
.= (p . u) + (0. L) by A11, A35, A36, FUNCT_4:12
.= p . u by RLVECT_1:def 7 ;
hence (p' + m) . u = p . u ; :: thesis: verum

end;

end;

end;

then eval p,x = eval (m + p'),x by A29, FUNCT_1:9
.= (eval p',x) + (eval m,x) by A19, Lm11 ;
hence (eval p,x) * (eval q,x) = ((eval p',x) * (eval q,x)) + ((eval m,x) * (eval q,x)) by VECTSP_1:def 18
.= (eval (p' *' q),x) + ((eval m,x) * (eval q,x)) by A5, A28
.= (eval (p' *' q),x) + (eval (m *' q),x) by A1, A19, Lm12
.= eval ((p' *' q) + (m *' q)),x by Th25
.= eval (q *' (p' + m)),x by POLYNOM1:85
.= eval (p *' q),x by A29, A30, FUNCT_1:9 ;
:: thesis: verum

end;

A37: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A4);
ex k being Element of NAT st card (Support p) = k ;
hence eval (p *' q),x = (eval p,x) * (eval q,x) by A37; :: thesis: verum