let a be real number ; :: thesis: for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)
let k, l be Integer; :: thesis: (a #Z k) #Z l = a #Z (k * l)

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

suppose A1: k * l > 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)

per cases ( ( k > 0 & l > 0 ) or ( k < 0 & l < 0 ) ) by A1, XREAL_1:136;

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

hence (a #Z k) #Z l = (a #Z k) |^ (abs l) by Def4
.= (a |^ (abs k)) |^ (abs l) by A2, Def4
.= a |^ ((abs k) * (abs l)) by NEWTON:14
.= a |^ (abs (k * l)) by COMPLEX1:151
.= a #Z (k * l) by A1, Def4 ;
:: thesis: verum

end;

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

hence (a #Z k) #Z l = ((a #Z k) |^ (abs l)) " by Def4
.= (((a |^ (abs k)) " ) |^ (abs l)) " by A3, Def4
.= ((1 / (a |^ (abs k))) |^ (abs l)) "
.= (1 / ((a |^ (abs k)) |^ (abs l))) " by Th14
.= (((a |^ (abs k)) |^ (abs l)) " ) "
.= a |^ ((abs k) * (abs l)) by NEWTON:14
.= a |^ (abs (k * l)) by COMPLEX1:151
.= a #Z (k * l) by A1, Def4 ;
:: thesis: verum

end;

end;

end;

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

per cases ( ( k < 0 & l > 0 ) or ( k > 0 & l < 0 ) ) by A4, XREAL_1:135;

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

hence (a #Z k) #Z l = (a #Z k) |^ (abs l) by Def4
.= ((a |^ (abs k)) " ) |^ (abs l) by A5, Def4
.= (1 / (a |^ (abs k))) |^ (abs l)
.= 1 / ((a |^ (abs k)) |^ (abs l)) by Th14
.= 1 / (a |^ ((abs k) * (abs l))) by NEWTON:14
.= 1 / (a |^ (abs (k * l))) by COMPLEX1:151
.= (a |^ (abs (k * l))) "
.= a #Z (k * l) by A4, Def4 ;
:: thesis: verum

end;

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

hence (a #Z k) #Z l = ((a #Z k) |^ (abs l)) " by Def4
.= ((a |^ (abs k)) |^ (abs l)) " by A6, Def4
.= (a |^ ((abs k) * (abs l))) " by NEWTON:14
.= (a |^ (abs (k * l))) " by COMPLEX1:151
.= a #Z (k * l) by A4, Def4 ;
:: thesis: verum

end;

end;

end;

suppose A7: k * l = 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)

per cases ( k = 0 or l = 0 ) by A7, XCMPLX_1:6;

suppose k = 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)

hence (a #Z k) #Z l = 1 #Z l by Th44
.= 1 by Th47
.= a #Z (k * l) by A7, Th44 ;
:: thesis: verum

end;

suppose l = 0 ; :: thesis: (a #Z k) #Z l = a #Z (k * l)

hence (a #Z k) #Z l = 1 by Th44
.= a #Z (k * l) by A7, Th44 ;
:: thesis: verum

end;

end;

end;

end;