let R be non degenerated comRing; :: thesis: for f being Series of 1,R holds f = (f * NBag1) * BagN1
let f be Series of 1,R; :: thesis: f = (f * NBag1) * BagN1
(f * NBag1) * BagN1 = f * (id (Bags 1)) by Th11, RELAT_1:36
.= f by FUNCT_2:17 ;
hence f = (f * NBag1) * BagN1 ; :: thesis: verum