let n be Element of NAT ; :: thesis: ( n >= 1 implies ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} ) )
assume A1: n >= 1 ; :: thesis: ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} )
A2: (#Z n) " {0} = {0}

proof

thus (#Z n) " {0} c= {0} :: according to XBOOLE_0:def 10 :: thesis: {0} c= (#Z n) " {0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (#Z n) " {0} or x in {0} )
assume A3: x in (#Z n) " {0} ; :: thesis: x in {0}
then reconsider x = x as Element of REAL ;
(#Z n) . x in {0} by A3, FUNCT_1:def 7;
then (#Z n) . x = 0 by TARSKI:def 1;
then x #Z n = 0 by TAYLOR_1:def 1;
then x |^ n = 0 by PREPOWER:36;
then x = 0 by PREPOWER:5;
hence x in {0} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {0} or x in (#Z n) " {0} )
A4: 0 in {0} by TARSKI:def 1;
assume x in {0} ; :: thesis: x in (#Z n) " {0}
then A5: x = 0 by TARSKI:def 1;
{(In (0,REAL))} c= REAL by ZFMISC_1:31;
then A6: {0} c= dom (#Z n) by FUNCT_2:def 1;
(#Z n) . 0 = 0 #Z n by TAYLOR_1:def 1
.= 0 |^ n by PREPOWER:36
.= 0 by A1, NEWTON:11 ;
hence x in (#Z n) " {0} by A5, A6, A4, FUNCT_1:def 7; :: thesis: verum

end;

then dom ((#Z n) ^) = (dom (#Z n)) \ {0} by RFUNCT_1:def 2
.= REAL \ {0} by FUNCT_2:def 1 ;
hence ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} ) by A2; :: thesis: verum