let R be non degenerated comRing; :: thesis: for f being Series of 1,R holds card (Support f) = card (Support (f * NBag1))
let f be Series of 1,R; :: thesis: card (Support f) = card (Support (f * NBag1))
card (Support f) = card (BagN1 .: (Support f)) by Th43
.= card (Support (f * NBag1)) by Th42 ;
hence card (Support f) = card (Support (f * NBag1)) ; :: thesis: verum