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

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

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

hence (a * b) #Z k = (a * b) |^ (abs k) by Def4
.= (a |^ (abs k)) * (b |^ (abs k)) by NEWTON:7
.= (a #Z k) * (b |^ (abs k)) by A1, Def4
.= (a #Z k) * (b #Z k) by A1, Def4 ;
:: thesis: verum

end;

suppose A2: k < 0 ; :: thesis: (a * b) #Z k = (a #Z k) * (b #Z k)

hence (a * b) #Z k = ((a * b) |^ (abs k)) " by Def4
.= ((a |^ (abs k)) * (b |^ (abs k))) " by NEWTON:7
.= ((a |^ (abs k)) ") * ((b |^ (abs k)) ") by XCMPLX_1:204
.= (a #Z k) * ((b |^ (abs k)) ") by A2, Def4
.= (a #Z k) * (b #Z k) by A2, Def4 ;
:: thesis: verum

end;

end;