let n be set ; :: thesis: for b being bag of n st b divides EmptyBag n holds
EmptyBag n = b
let b be bag of n; :: thesis: ( b divides EmptyBag n implies EmptyBag n = b )
assume A1: b divides EmptyBag n ; :: thesis: EmptyBag n = b

now

let k be set ; :: thesis: ( k in n implies (EmptyBag n) . k = b . k )
assume k in n ; :: thesis: (EmptyBag n) . k = b . k
(EmptyBag n) . k = 0 by Th52;
hence (EmptyBag n) . k = b . k by A1, Def11; :: thesis: verum

end;

hence EmptyBag n = b by PBOOLE:3; :: thesis: verum