let R be non degenerated comRing; :: thesis: for f being sequence of the carrier of R holds f = (f * BagN1) * NBag1
let f be sequence of the carrier of R; :: thesis: f = (f * BagN1) * NBag1
(f * BagN1) * NBag1 = f * (id NAT) by Th10, RELAT_1:36
.= f by FUNCT_2:17 ;
hence f = (f * BagN1) * NBag1 ; :: thesis: verum