let a be Real; :: 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:134;

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) |^ |.l.| by Def3
.= (a |^ |.k.|) |^ |.l.| by A2, Def3
.= a |^ (|.k.| * |.l.|) by NEWTON:9
.= a |^ |.(k * l).| by COMPLEX1:65
.= a #Z (k * l) by A1, Def3 ;
:: 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) |^ |.l.|) " by Def3
.= (((a |^ |.k.|) ") |^ |.l.|) " by A3, Def3
.= ((1 / (a |^ |.k.|)) |^ |.l.|) "
.= (1 / ((a |^ |.k.|) |^ |.l.|)) " by Th7
.= (((a |^ |.k.|) |^ |.l.|) ") "
.= a |^ (|.k.| * |.l.|) by NEWTON:9
.= a |^ |.(k * l).| by COMPLEX1:65
.= a #Z (k * l) by A1, Def3 ;
:: 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:133;

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) |^ |.l.| by Def3
.= ((a |^ |.k.|) ") |^ |.l.| by A5, Def3
.= (1 / (a |^ |.k.|)) |^ |.l.|
.= 1 / ((a |^ |.k.|) |^ |.l.|) by Th7
.= 1 / (a |^ (|.k.| * |.l.|)) by NEWTON:9
.= 1 / (a |^ |.(k * l).|) by COMPLEX1:65
.= (a |^ |.(k * l).|) "
.= a #Z (k * l) by A4, Def3 ;
:: 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) |^ |.l.|) " by Def3
.= ((a |^ |.k.|) |^ |.l.|) " by A6, Def3
.= (a |^ (|.k.| * |.l.|)) " by NEWTON:9
.= (a |^ |.(k * l).|) " by COMPLEX1:65
.= a #Z (k * l) by A4, Def3 ;
:: 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;

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

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

end;

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

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

end;

end;

end;

end;