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 } )
A0: (#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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (#Z n) " {0 } or x in {0 } )
assume A7: x in (#Z n) " {0 } ; :: thesis: x in {0 }
then reconsider x = x as Element of REAL ;
(#Z n) . x in {0 } by A7, FUNCT_1:def 13;
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:46;
then x = 0 by PREPOWER:12;
hence x in {0 } by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {0 } or x in (#Z n) " {0 } )
assume x in {0 } ; :: thesis: x in (#Z n) " {0 }
then A2: x = 0 by TARSKI:def 1;
{0 } c= REAL by ZFMISC_1:37;
then A3: {0 } c= dom (#Z n) by FUNCT_2:def 1;
A4: 0 in {0 } by TARSKI:def 1;
(#Z n) . 0 = 0 #Z n by TAYLOR_1:def 1
.= 0 |^ n by PREPOWER:46
.= 0 by A1, NEWTON:16 ;
hence x in (#Z n) " {0 } by A2, A4, A3, FUNCT_1:def 13; :: thesis: verum

end;

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