per cases ( f is empty or not f is empty ) ;

suppose f is empty ; :: thesis: MeanMore f is empty

then dom f = {} ;
then MeanMore f c= {} by MoreDom;
hence MeanMore f is empty ; :: thesis: verum

end;

suppose AA: not f is empty ; :: thesis: MeanMore f is empty

A0: HetSet f = (MeanLess f) \/ (MeanMore f) by MeanSum;
MeanMore f = {}

proof

assume MeanMore f <> {} ; :: thesis: contradiction
then consider x being object such that
A1: x in MeanMore f by XBOOLE_0:7;
Het f <> 0 by A0, A1;
hence contradiction by HetHetero, AA; :: thesis: verum

end;

hence MeanMore f is empty ; :: thesis: verum

end;

end;