let a, b be Real; :: 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) |^ |.k.| by Def3
.= (a |^ |.k.|) * (b |^ |.k.|) by NEWTON:7
.= (a #Z k) * (b |^ |.k.|) by A1, Def3
.= (a #Z k) * (b #Z k) by A1, Def3 ;
:: 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) |^ |.k.|) " by Def3
.= ((a |^ |.k.|) * (b |^ |.k.|)) " by NEWTON:7
.= ((a |^ |.k.|) ") * ((b |^ |.k.|) ") by XCMPLX_1:204
.= (a #Z k) * ((b |^ |.k.|) ") by A2, Def3
.= (a #Z k) * (b #Z k) by A2, Def3 ;
:: thesis: verum

end;

end;