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 p, q 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 p, q 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, q 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);
A1: 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 A2: p = 0_ n,L by Th19;
hence eval (p *' q),x = eval p,x by POLYNOM1:87
.= 0. L by A2, Th22
.= (0. L) * (eval q,x) by VECTSP_1:39
.= (eval p,x) * (eval q,x) by A2, Th22 ;
:: thesis: verum

end;

A3: 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 A4: 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 A5: 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)))));
A6: BagOrder n linearly_orders Support p by Th20;
then rng (SgmX (BagOrder n),(Support p)) <> {} by A5, 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 A7: 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 A7, FUNCT_1:def 5;
then A8: (SgmX (BagOrder n),(Support p)) /. (len (SgmX (BagOrder n),(Support p))) in Support p by A6, TRIANG_1:def 2;
then A9: 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 A10: 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 A11: 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 A12: 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 A10, A12, FUNCT_4:14;
then p' . u = 0. L by FUNCOP_1:87;
hence contradiction by A11, 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 A10, FUNCT_4:12;
then p . u <> 0. L by A11, 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 A13: (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 ;
A14: 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 A15: u in Support m ; :: thesis: u in {bg}
then reconsider u = u as Element of Bags n ;
A16: m . u <> 0. L by A15, 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 A13, FUNCT_4:12;
hence contradiction by A16, 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 A17: 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 A13, FUNCT_4:14;
then m . bg = p . bg by FUNCOP_1:87;
hence u in Support m by A9, A17, POLYNOM1:def 9; :: thesis: verum

end;

then A18: Support m = {bg} by A14, 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 A10, FUNCT_4:14;
then A19: p' . bg = 0. L by FUNCOP_1:87;
then A20: not bg in Support p' by POLYNOM1:def 9;
A21: 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 A22: u in Support p ; :: thesis: u in (Support p') \/ {bg}
then reconsider u = u as Element of Bags n ;
A23: p . u <> 0. L by A22, 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 A10, FUNCT_4:12;
then u in Support p' by A23, 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 A24: u in (Support p') \/ {bg} ; :: thesis: u in Support p

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

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

then reconsider u = u as Element of Bags n ;
A26: p' . u <> 0. L by A25, POLYNOM1:def 9;
u <> bg by A19, A25, 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 A10, FUNCT_4:12;
hence u in Support p by A26, POLYNOM1:def 9; :: thesis: verum

end;

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

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

end;

end;

end;

then Support p = (Support p') \/ {bg} by A21, TARSKI:2;
then A27: k + 1 = (card (Support p')) + 1 by A5, A20, CARD_2:54;
A28: ( dom (p' + m) = Bags n & dom p = Bags n ) by FUNCT_2:def 1;
A29: 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 A30: 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 A31: p' . u = (bg .--> (0. L)) . bg by A10, A30, 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 A13, FUNCT_4:14;
then A32: m . bg = p . bg by FUNCOP_1:87;
(p' + m) . u = (p' . u) + (m . u) by POLYNOM1:def 21
.= (0. L) + (p . bg) by A30, A31, A32, FUNCOP_1:87
.= p . bg by RLVECT_1:def 7 ;
hence (p' + m) . u = p . u by A30; :: thesis: verum

end;

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

then A33: not u in {bg} by TARSKI:def 1;
then A34: not u in dom (bg .--> (0. L)) by FUNCOP_1:19;
not u in dom (bg .--> (p . bg)) by A33, FUNCOP_1:19;
then m . u = (0_ n,L) . u by A13, FUNCT_4:12;
then A35: m . u = 0. L by POLYNOM1:81;
(p' + m) . u = (p' . u) + (m . u) by POLYNOM1:def 21
.= (p . u) + (0. L) by A10, A34, A35, 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 A28, FUNCT_1:9
.= (eval p',x) + (eval m,x) by A18, 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 A4, A27
.= (eval (p' *' q),x) + (eval (m *' q),x) by A18, Lm13
.= eval ((p' *' q) + (m *' q)),x by Th25
.= eval (q *' (p' + m)),x by POLYNOM1:85
.= eval (p *' q),x by A28, A29, FUNCT_1:9 ;
:: thesis: verum

end;

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