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;