let b be bag of 1; :: thesis: b = 1 --> (b . 0)
for o being object st o in dom b holds
b . o = (1 --> (b . 0)) . o

proof

let o be object ; :: thesis: ( o in dom b implies b . o = (1 --> (b . 0)) . o )
assume A1: o in dom b ; :: thesis: b . o = (1 --> (b . 0)) . o
then o = 0 by CARD_1:49, TARSKI:def 1;
hence b . o = (1 --> (b . 0)) . o by A1, FUNCOP_1:7; :: thesis: verum

end;

hence b = 1 --> (b . 0) by PARTFUN1:def 2; :: thesis: verum