let b1, b2 be bag of 1; :: thesis: b1 -' b2 = 1 --> ((b1 . 0) -' (b2 . 0))
reconsider b = b1 -' b2 as bag of 1 ;
A1: dom (b1 -' b2) = {0} by Th4
.= dom (1 --> ((b1 . 0) -' (b2 . 0))) by Th4 ;
for x being object st x in dom (b1 -' b2) holds
(b1 -' b2) . x = (1 --> ((b1 . 0) -' (b2 . 0))) . x

proof

let x be object ; :: thesis: ( x in dom (b1 -' b2) implies (b1 -' b2) . x = (1 --> ((b1 . 0) -' (b2 . 0))) . x )
assume A2: x in dom (b1 -' b2) ; :: thesis: (b1 -' b2) . x = (1 --> ((b1 . 0) -' (b2 . 0))) . x
then x in {0} by Th4;
then (b1 -' b2) . x = (b1 -' b2) . 0 by TARSKI:def 1
.= (b1 . 0) -' (b2 . 0) by PRE_POLY:def 6
.= (1 --> ((b1 . 0) -' (b2 . 0))) . x by A2, FUNCOP_1:7 ;
hence (b1 -' b2) . x = (1 --> ((b1 . 0) -' (b2 . 0))) . x ; :: thesis: verum

end;

hence b1 -' b2 = 1 --> ((b1 . 0) -' (b2 . 0)) by A1; :: thesis: verum