let X be set ; :: thesis: for b1, b2 being bag of X st (2 (#) b1) +* (0,(b1 . 0)) = (2 (#) b2) +* (0,(b2 . 0)) holds
b1 = b2
let b1, b2 be bag of X; :: thesis: ( (2 (#) b1) +* (0,(b1 . 0)) = (2 (#) b2) +* (0,(b2 . 0)) implies b1 = b2 )
assume A1: (2 (#) b1) +* (0,(b1 . 0)) = (2 (#) b2) +* (0,(b2 . 0)) ; :: thesis: b1 = b2
A2: ( dom b1 = X & X = dom b2 & dom (2 (#) b1) = X & X = dom (2 (#) b2) ) by PARTFUN1:def 2;
for x being object st x in X holds
b1 . x = b2 . x

proof

let x be object ; :: thesis: ( x in X implies b1 . x = b2 . x )
assume A3: x in X ; :: thesis: b1 . x = b2 . x

per cases ( x = 0 or x <> 0 ) ;

suppose A4: x = 0 ; :: thesis: b1 . x = b2 . x

hence b1 . x = ((2 (#) b1) +* (0,(b1 . 0))) . x by A3, A2, FUNCT_7:31
.= b2 . x by A4, A3, A2, A1, FUNCT_7:31 ;
:: thesis: verum

end;

suppose A5: x <> 0 ; :: thesis: b1 . x = b2 . x

2 * (b1 . x) = (2 (#) b1) . x by A2, A3, VALUED_1:def 5
.= ((2 (#) b1) +* (0,(b1 . 0))) . x by A5, FUNCT_7:32
.= (2 (#) b2) . x by A5, A1, FUNCT_7:32
.= 2 * (b2 . x) by A3, A2, VALUED_1:def 5 ;
hence b1 . x = b2 . x ; :: thesis: verum

end;

end;

end;

hence b1 = b2 by A2; :: thesis: verum