let I be set ; :: thesis: ( I = support m iff I = m " (NAT \ {0}) )
support m = m " (NAT \ {0})

proof

thus support m c= m " (NAT \ {0}) :: according to XBOOLE_0:def 10 :: thesis: m " (NAT \ {0}) c= support m

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in support m or a in m " (NAT \ {0}) )
assume a in support m ; :: thesis: a in m " (NAT \ {0})
then A1: m . a <> 0 by PRE_POLY:def 7;
then A2: a in dom m by FUNCT_1:def 2;
( m . a in NAT & not m . a in {0} ) by A1, TARSKI:def 1, ORDINAL1:def 12;
then m . a in NAT \ {0} by XBOOLE_0:def 5;
hence a in m " (NAT \ {0}) by A2, FUNCT_1:def 7; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in m " (NAT \ {0}) or a in support m )
assume a in m " (NAT \ {0}) ; :: thesis: a in support m
then m . a in NAT \ {0} by FUNCT_1:def 7;
then not m . a in {0} by XBOOLE_0:def 5;
then m . a <> 0 by TARSKI:def 1;
hence a in support m by PRE_POLY:def 7; :: thesis: verum

end;

hence ( I = support m iff I = m " (NAT \ {0}) ) ; :: thesis: verum