let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L holds (EmptyBag n) *' p = p
let T be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds (EmptyBag n) *' p = p
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds (EmptyBag n) *' p = p
let p be Series of n,L; :: thesis: (EmptyBag n) *' p = p
set e = EmptyBag n;

A1: now

let u be set ; :: thesis: ( u in dom p implies ((EmptyBag n) *' p) . u = p . u )
assume u in dom p ; :: thesis: ((EmptyBag n) *' p) . u = p . u
then reconsider u9 = u as Element of Bags n ;
EmptyBag n divides u9 by PRE_POLY:59;
then ((EmptyBag n) *' p) . u9 = p . (u9 -' (EmptyBag n)) by Def1
.= p . u9 by PRE_POLY:54 ;
hence ((EmptyBag n) *' p) . u = p . u ; :: thesis: verum

end;

dom ((EmptyBag n) *' p) = Bags n by FUNCT_2:def 1
.= dom p by FUNCT_2:def 1 ;
hence (EmptyBag n) *' p = p by A1, FUNCT_1:2; :: thesis: verum