let R be non degenerated comRing; :: thesis: for f being sequence of R holds card (Support f) = card (Support (f * BagN1))
let f be sequence of R; :: thesis: card (Support f) = card (Support (f * BagN1))
card (Support f) = card (NBag1 .: (Support f)) by Th40
.= card (Support (f * BagN1)) by Th39 ;
hence card (Support f) = card (Support (f * BagN1)) ; :: thesis: verum