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 n 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 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 n 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 n 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 n 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₁[ 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: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: 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 A4: 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))));
A5: BagOrder n linearly_orders Support p by Th10;
then SgmX ((BagOrder n),(Support p)) <> {} by A4, CARD_1:27, PRE_POLY:def 2, RELAT_1:38;
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:1;
then A6: 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 6;
then (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) in rng (SgmX ((BagOrder n),(Support p))) by A6, FUNCT_1:def 3;
then A7: (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) in Support p by A5, PRE_POLY:def 2;
then A8: p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))) <> 0. L by POLYNOM1:def 4;
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)))))));
set p9 = p +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(0. L));
reconsider bg = (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) as bag of n ;
dom p = Bags n by FUNCT_2:def 1;
then A9: p +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(0. L)) = p +* (bg .--> (0. L)) by FUNCT_7:def 3;
reconsider p9 = p +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(0. L)) as Function of (Bags n), the carrier of L ;
reconsider p9 = p9 as Function of (Bags n),L ;
for u being object st u in Support p9 holds
u in Support p

proof

let u be object ; :: thesis: ( u in Support p9 implies u in Support p )
assume A10: u in Support p9 ; :: thesis: u in Support p
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of n ;

now :: thesis: not u = bg

assume A11: u = bg ; :: thesis: contradiction
then u in {bg} by TARSKI:def 1;
then u in dom (bg .--> (0. L)) ;
then p9 . u = (bg .--> (0. L)) . bg by A9, A11, FUNCT_4:13;
then p9 . u = 0. L by FUNCOP_1:72;
hence contradiction by A10, POLYNOM1:def 4; :: thesis: verum

end;

then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) ;
then p . u = p9 . u by A9, FUNCT_4:11;
then p . u <> 0. L by A10, POLYNOM1:def 4;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum

end;

then Support p9 c= Support p by TARSKI:def 3;
then reconsider p9 = p9 as Polynomial of n,L by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object st u in Support p holds
u in (Support p9) \/ {bg}

proof

let u be object ; :: thesis: ( u in Support p implies u in (Support p9) \/ {bg} )
assume A14: u in Support p ; :: thesis: u in (Support p9) \/ {bg}
then reconsider u = u as Element of Bags n ;
A15: p . u <> 0. L by A14, POLYNOM1:def 4;

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

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

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

end;

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

then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) ;
then p9 . u = p . u by A9, FUNCT_4:11;
then u in Support p9 by A15, POLYNOM1:def 4;
hence u in (Support p9) \/ {bg} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (0. L)) ;
then p9 . bg = (bg .--> (0. L)) . bg by A9, FUNCT_4:13;
then A16: p9 . bg = 0. L by FUNCOP_1:72;
then A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object st u in (Support p9) \/ {bg} holds
u in Support p

proof

let u be object ; :: thesis: ( u in (Support p9) \/ {bg} implies u in Support p )
assume A18: u in (Support p9) \/ {bg} ; :: thesis: u in Support p

per cases ( u in Support p9 or u in {bg} ) by A18, XBOOLE_0:def 3;

suppose A19: u in Support p9 ; :: thesis: u in Support p

then reconsider u = u as Element of Bags n ;
u <> bg by A16, A19, POLYNOM1:def 4;
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (0. L)) ;
then A20: p9 . u = p . u by A9, FUNCT_4:11;
p9 . u <> 0. L by A19, POLYNOM1:def 4;
hence u in Support p by A20, POLYNOM1:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

then Support p = (Support p9) \/ {bg} by A13, TARSKI:2;
then A21: k + 1 = (card (Support p9)) + 1 by A4, A17, CARD_2:41;
dom (0_ (n,L)) = Bags n by FUNCT_2:def 1;
then A22: (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 ;
A23: for u being object st u in Support m holds
u in {bg}

proof

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

now :: thesis: not u <> bg

assume u <> bg ; :: thesis: contradiction
then not u in {bg} by TARSKI:def 1;
then not u in dom (bg .--> (p . bg)) ;
then m . u = (0_ (n,L)) . u by A22, FUNCT_4:11;
hence contradiction by A25, POLYNOM1:22; :: thesis: verum

end;

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

end;

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

proof

let u be object ; :: thesis: ( u in {bg} implies u in Support m )
bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) ;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A26: m . bg = p . bg by FUNCOP_1:72;
assume u in {bg} ; :: thesis: u in Support m
then u = bg by TARSKI:def 1;
hence u in Support m by A8, A26, POLYNOM1:def 4; :: thesis: verum

end;

then A27: Support m = {bg} by A23, TARSKI:2;
then reconsider m = m as Polynomial of n,L by POLYNOM1:def 5;
reconsider m = m as Polynomial of n,L ;
A28: for u being object st u in Bags n holds
(p9 + m) . u = p . u

proof

let u be object ; :: thesis: ( u in Bags n implies (p9 + m) . u = p . u )
assume u in Bags n ; :: thesis: (p9 + m) . u = p . u
then reconsider u = u as bag of n ;

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

suppose A29: u = bg ; :: thesis: (p9 + m) . u = p . u

bg in {bg} by TARSKI:def 1;
then bg in dom (bg .--> (p . bg)) ;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A30: m . bg = p . bg by FUNCOP_1:72;
u in {bg} by A29, TARSKI:def 1;
then u in dom (bg .--> (0. L)) ;
then A31: p9 . u = (bg .--> (0. L)) . bg by A9, A29, FUNCT_4:13;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:15
.= (0. L) + (p . bg) by A29, A31, A30, FUNCOP_1:72
.= p . bg by RLVECT_1:def 4 ;
hence (p9 + m) . u = p . u by A29; :: thesis: verum

end;

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

then A32: not u in {bg} by TARSKI:def 1;
then A33: not u in dom (bg .--> (0. L)) ;
not u in dom (bg .--> (p . bg)) by A32;
then m . u = (0_ (n,L)) . u by A22, FUNCT_4:11;
then A34: m . u = 0. L by POLYNOM1:22;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:15
.= (p . u) + (0. L) by A9, A33, A34, FUNCT_4:11
.= p . u by RLVECT_1:def 4 ;
hence (p9 + m) . u = p . u ; :: thesis: verum

end;

end;

end;

A35: dom (p9 + m) = Bags n by FUNCT_2:def 1;
then eval (p,x) = eval ((m + p9),x) by A12, A28, FUNCT_1:2
.= (eval (p9,x)) + (eval (m,x)) by A27, Lm7 ;
hence (eval (p,x)) * (eval (q,x)) = ((eval (p9,x)) * (eval (q,x))) + ((eval (m,x)) * (eval (q,x))) by VECTSP_1:def 7
.= (eval ((p9 *' q),x)) + ((eval (m,x)) * (eval (q,x))) by A3, A21
.= (eval ((p9 *' q),x)) + (eval ((m *' q),x)) by A1, A27, Lm8
.= eval (((p9 *' q) + (m *' q)),x) by Th15
.= eval ((q *' (p9 + m)),x) by POLYNOM1:26
.= eval ((p *' q),x) by A35, A12, A28, FUNCT_1:2 ;
:: thesis: verum

end;

A36: ex k being Element of NAT st card (Support p) = k ;
A37: 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 A38: p = 0_ (n,L) by Th9;
hence eval ((p *' q),x) = eval (p,x) by POLYNOM1:28
.= (0. L) * (eval (q,x)) by A38, Th12
.= (eval (p,x)) * (eval (q,x)) by A38, Th12 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A37, A2);
hence eval ((p *' q),x) = (eval (p,x)) * (eval (q,x)) by A36; :: thesis: verum