let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g
let f, g be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g
let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A, B being LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds
A ^ B is_MonomialRepresentation_of f + g
let A, B be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g implies A ^ B is_MonomialRepresentation_of f + g )
assume that
A1: A is_MonomialRepresentation_of f and
A2: B is_MonomialRepresentation_of g ; :: thesis: A ^ B is_MonomialRepresentation_of f + g

A3: now :: thesis: for i being Element of NAT st i in dom (A ^ B) holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p )

let i be Element of NAT ; :: thesis: ( i in dom (A ^ B) implies ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p ) )
assume A4: i in dom (A ^ B) ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p )

now :: thesis: ( ( i in dom A & ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p ) ) or ( ex k being Nat st
( k in dom B & i = (len A) + k ) & ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p ) ) )

per cases ( i in dom A or ex k being Nat st
( k in dom B & i = (len A) + k ) ) by A4, FINSEQ_1:25;

case A5: i in dom A ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p )

dom A c= dom (A ^ B) by FINSEQ_1:26;
then (A ^ B) /. i = (A ^ B) . i by A5, PARTFUN1:def 6
.= A . i by A5, FINSEQ_1:def 7
.= A /. i by A5, PARTFUN1:def 6 ;
hence ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p ) by A1, A5; :: thesis: verum

end;

case ex k being Nat st
( k in dom B & i = (len A) + k ) ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p )

then consider k being Nat such that
A6: k in dom B and
A7: i = (len A) + k ;
i in dom (A ^ B) by A6, A7, FINSEQ_1:28;
then (A ^ B) /. i = (A ^ B) . i by PARTFUN1:def 6
.= B . k by A6, A7, FINSEQ_1:def 7
.= B /. k by A6, PARTFUN1:def 6 ;
hence ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p ) by A2, A6; :: thesis: verum

end;

end;

end;

hence ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & (A ^ B) /. i = m *' p ) ; :: thesis: verum

end;

reconsider f9 = f, g9 = g as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider f9 = f9, g9 = g9 as Element of (Polynom-Ring (n,L)) ;
Sum (A ^ B) = (Sum A) + (Sum B) by RLVECT_1:41
.= f9 + (Sum B) by A1
.= f9 + g9 by A2
.= f + g by POLYNOM1:def 11 ;
hence A ^ B is_MonomialRepresentation_of f + g by A3; :: thesis: verum