let a be Real; :: 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 |^ |.(k + l).| by A2, Def3
.= a |^ (|.k.| + |.l.|) by A3, ABSVALUE:11
.= (a |^ |.k.|) * (a |^ |.l.|) by NEWTON:8
.= (a #Z k) * (a |^ |.l.|) by A2, Def3
.= (a #Z k) * (a #Z l) by A2, Def3 ; :: 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, Th43
.= (a |^ m) * ((a |^ n) ")
.= (a |^ |.k.|) * ((a |^ n) ") by ABSVALUE:def 1
.= (a |^ |.k.|) * ((a |^ |.(- l).|) ") by ABSVALUE:def 1
.= (a |^ |.k.|) * ((a |^ |.l.|) ") by COMPLEX1:52
.= (a #Z k) * ((a |^ |.l.|) ") by A4, Def3
.= (a #Z k) * (a #Z l) by A4, Def3 ;
:: 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, Th43
.= (a |^ m) * ((a |^ n) ")
.= (a |^ |.l.|) * ((a |^ n) ") by ABSVALUE:def 1
.= (a |^ |.l.|) * ((a |^ |.(- k).|) ") by ABSVALUE:def 1
.= (a |^ |.l.|) * ((a |^ |.k.|) ") by COMPLEX1:52
.= (a #Z l) * ((a |^ |.k.|) ") by A5, Def3
.= (a #Z k) * (a #Z l) by A5, Def3 ;
:: 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 |^ |.(k + l).|) " by A6, Def3
.= (a |^ (|.k.| + |.l.|)) " by A7, ABSVALUE:11
.= ((a |^ |.k.|) * (a |^ |.l.|)) " by NEWTON:8
.= ((a |^ |.k.|) ") * ((a |^ |.l.|) ") by XCMPLX_1:204
.= (a #Z k) * ((a |^ |.l.|) ") by A6, Def3
.= (a #Z k) * (a #Z l) by A6, Def3 ; :: thesis: verum

end;

end;