let a be Real; :: thesis: for m, n being Nat st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)
let m, n be Nat; :: 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:3;
A2: (a #Z (m - n)) * (a |^ n) = (a |^ m1) * (a |^ n) by Th36
.= a |^ (m1 + n) by NEWTON:8
.= a |^ m ;
a |^ n <> 0 by A1, Th5;
hence a #Z (m - n) = (a |^ m) / (a |^ n) by A2, XCMPLX_1:89; :: thesis: verum

end;

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

then - (m - n) > 0 ;
then reconsider m1 = n - m as Element of NAT by INT_1:3;
A3: a #Z (n - m) = a #Z (- (m - n))
.= 1 / (a #Z (m - n)) by Th41 ;
(a #Z (n - m)) * (a |^ m) = (a |^ m1) * (a |^ m) by Th36
.= a |^ (m1 + m) by NEWTON:8
.= a |^ n ;
then A4: (a |^ m) / (a #Z (m - n)) = a |^ n by A3;
a |^ n <> 0 by A1, Th5;
hence a #Z (m - n) = (a |^ m) / (a |^ n) by A4, XCMPLX_1:54; :: thesis: verum

end;

end;