let a be real number ; :: thesis: for k, l being Integer st a <> 0 holds
a #Z (k + l) = (a #Z k) * (a #Z l)
let k, l be Integer; :: thesis: ( a <> 0 implies a #Z (k + l) = (a #Z k) * (a #Z l) )
assume A1: a <> 0 ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

per cases ( ( k >= 0 & l >= 0 ) or ( k >= 0 & l < 0 ) or ( k < 0 & l >= 0 ) or ( k < 0 & l < 0 ) ) ;

suppose A2: ( k >= 0 & l >= 0 ) ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then A3: k * l >= 0 ;
thus a #Z (k + l) = a |^ (abs (k + l)) by A2, Def4
.= a |^ ((abs k) + (abs l)) by A3, ABSVALUE:11
.= (a |^ (abs k)) * (a |^ (abs l)) by NEWTON:8
.= (a #Z k) * (a |^ (abs l)) by A2, Def4
.= (a #Z k) * (a #Z l) by A2, Def4 ; :: thesis: verum

end;

suppose A4: ( k >= 0 & l < 0 ) ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then reconsider m = k as Element of NAT by INT_1:3;
reconsider n = - l as Element of NAT by A4, INT_1:3;
k + l = m - n ;
hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th53
.= (a |^ m) * ((a |^ n) ")
.= (a |^ (abs k)) * ((a |^ n) ") by ABSVALUE:def 1
.= (a |^ (abs k)) * ((a |^ (abs (- l))) ") by ABSVALUE:def 1
.= (a |^ (abs k)) * ((a |^ (abs l)) ") by COMPLEX1:52
.= (a #Z k) * ((a |^ (abs l)) ") by A4, Def4
.= (a #Z k) * (a #Z l) by A4, Def4 ;
:: thesis: verum

end;

suppose A5: ( k < 0 & l >= 0 ) ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then reconsider m = l as Element of NAT by INT_1:3;
reconsider n = - k as Element of NAT by A5, INT_1:3;
k + l = m - n ;
hence a #Z (k + l) = (a |^ m) / (a |^ n) by A1, Th53
.= (a |^ m) * ((a |^ n) ")
.= (a |^ (abs l)) * ((a |^ n) ") by ABSVALUE:def 1
.= (a |^ (abs l)) * ((a |^ (abs (- k))) ") by ABSVALUE:def 1
.= (a |^ (abs l)) * ((a |^ (abs k)) ") by COMPLEX1:52
.= (a #Z l) * ((a |^ (abs k)) ") by A5, Def4
.= (a #Z k) * (a #Z l) by A5, Def4 ;
:: thesis: verum

end;

suppose A6: ( k < 0 & l < 0 ) ; :: thesis: a #Z (k + l) = (a #Z k) * (a #Z l)

then A7: k * l >= 0 ;
thus a #Z (k + l) = (a |^ (abs (k + l))) " by A6, Def4
.= (a |^ ((abs k) + (abs l))) " by A7, ABSVALUE:11
.= ((a |^ (abs k)) * (a |^ (abs l))) " by NEWTON:8
.= ((a |^ (abs k)) ") * ((a |^ (abs l)) ") by XCMPLX_1:204
.= (a #Z k) * ((a |^ (abs l)) ") by A6, Def4
.= (a #Z k) * (a #Z l) by A6, Def4 ; :: thesis: verum

end;

end;