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: dom ((EmptyBag n) *' p) = Bags n by FUNCT_2:def 1
.= dom p by FUNCT_2:def 1 ;

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 u' = u as Element of Bags n ;
EmptyBag n divides u' by POLYNOM1:63;
then ((EmptyBag n) *' p) . u' = p . (u' -' (EmptyBag n)) by Def1
.= p . u' by POLYNOM1:58 ;
hence ((EmptyBag n) *' p) . u = p . u ; :: thesis: verum

end;

hence (EmptyBag n) *' p = p by A1, FUNCT_1:9; :: thesis: verum