let X, x be set ; :: thesis: (EmptyBag X) . x = 0
A1: dom (X --> 0 ) = X by FUNCOP_1:19;

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: (EmptyBag X) . x = 0

hence (EmptyBag X) . x = 0 by FUNCOP_1:13; :: thesis: verum

end;

suppose not x in X ; :: thesis: (EmptyBag X) . x = 0

hence (EmptyBag X) . x = 0 by A1, FUNCT_1:def 4; :: thesis: verum

end;

end;