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:24
.= (a |^ (abs k)) * (a |^ (abs l)) by NEWTON:13
.= (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:16;
reconsider n = - l as Element of NAT by A4, INT_1:16;
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:138
.= (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:16;
reconsider n = - k as Element of NAT by A5, INT_1:16;
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:138
.= (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:24
.= ((a |^ (abs k)) * (a |^ (abs l))) " by NEWTON:13
.= ((a |^ (abs k)) " ) * ((a |^ (abs l)) " ) by XCMPLX_1:205
.= (a #Z k) * ((a |^ (abs l)) " ) by A6, Def4
.= (a #Z k) * (a #Z l) by A6, Def4 ; :: thesis: verum

end;

end;