let a be real number ; :: thesis: for m, n being natural number st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)
let m, n be natural number ; :: thesis: ( a <> 0 implies a #Z (m - n) = (a |^ m) / (a |^ n) )
assume A1: a <> 0 ; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

per cases ( m - n >= 0 or m - n < 0 ) ;

suppose m - n >= 0 ; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

then reconsider m1 = m - n as Element of NAT by INT_1:16;
A2: (a #Z (m - n)) * (a |^ n) = (a |^ m1) * (a |^ n) by Th46
.= a |^ (m1 + n) by NEWTON:13
.= a |^ m ;
a |^ n <> 0 by A1, Th12;
hence a #Z (m - n) = (a |^ m) / (a |^ n) by A2, XCMPLX_1:90; :: thesis: verum

end;

suppose m - n < 0 ; :: thesis: a #Z (m - n) = (a |^ m) / (a |^ n)

then - (m - n) > 0 by XREAL_1:60;
then reconsider m1 = n - m as Element of NAT by INT_1:16;
A3: a #Z (n - m) = a #Z (- (m - n))
.= 1 / (a #Z (m - n)) by Th51 ;
(a #Z (n - m)) * (a |^ m) = (a |^ m1) * (a |^ m) by Th46
.= a |^ (m1 + m) by NEWTON:13
.= a |^ n ;
then A4: (a |^ m) / (a #Z (m - n)) = a |^ n by A3;
a |^ n <> 0 by A1, Th12;
hence a #Z (m - n) = (a |^ m) / (a |^ n) by A4, XCMPLX_1:54; :: thesis: verum

end;

end;