let n be Ordinal; :: thesis: for L being non empty 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 empty 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 A1: ( A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g ) ; :: thesis: A ^ B is_MonomialRepresentation_of f + g
reconsider f' = f, g' = g as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider f' = f', g' = g' as Element of (Polynom-Ring n,L) ;
A2: Sum (A ^ B) = (Sum A) + (Sum B) by RLVECT_1:58
.= f' + (Sum B) by A1, Def6
.= f' + g' by A1, Def6
.= f + g by POLYNOM1:def 27 ;

now

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 A3: 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

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

case A4: 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:39;
then (A ^ B) /. i = (A ^ B) . i by A4, PARTFUN1:def 8
.= A . i by A4, FINSEQ_1:def 7
.= A /. i by A4, PARTFUN1:def 8 ;
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, A4, Def6; :: 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
A5: ( k in dom B & i = (len A) + k ) ;
i in dom (A ^ B) by A5, FINSEQ_1:41;
then (A ^ B) /. i = (A ^ B) . i by PARTFUN1:def 8
.= B . k by A5, FINSEQ_1:def 7
.= B /. k by A5, PARTFUN1:def 8 ;
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, Def6; :: 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;

hence A ^ B is_MonomialRepresentation_of f + g by A2, Def6; :: thesis: verum