let L be comRing; :: thesis: for a being Element of L
for p being non empty FinSequence of the carrier of L st ( for j being Nat st j in dom p holds
a divides p /. j ) holds
a divides Sum p
let a be Element of L; :: thesis: for p being non empty FinSequence of the carrier of L st ( for j being Nat st j in dom p holds
a divides p /. j ) holds
a divides Sum p
let p be non empty FinSequence of the carrier of L; :: thesis: ( ( for j being Nat st j in dom p holds
a divides p /. j ) implies a divides Sum p )
assume A1: for j being Nat st j in dom p holds
a divides p /. j ; :: thesis: a divides Sum p
for i being Nat st i in dom p holds
p . i in {a} -Ideal

proof

let i be Nat; :: thesis: ( i in dom p implies p . i in {a} -Ideal )
assume A3: i in dom p ; :: thesis: p . i in {a} -Ideal
then p . i = p /. i by PARTFUN1:def 6;
hence p . i in {a} -Ideal by A1, A3, RING_2:18; :: thesis: verum

end;

hence a divides Sum p by RING_2:18, Th13; :: thesis: verum