let n be set ; :: thesis: for S being non empty ZeroStr
for b being bag of n holds (0_ (n,S)) . b = 0. S
let S be non empty ZeroStr ; :: thesis: for b being bag of n holds (0_ (n,S)) . b = 0. S
let b be bag of n; :: thesis: (0_ (n,S)) . b = 0. S
b in Bags n by PRE_POLY:def 12;
hence (0_ (n,S)) . b = 0. S by FUNCOP_1:7; :: thesis: verum