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)

let k be Integer; :: thesis: (a * b) #Z k = (a #Z k) * (b #Z k)

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

end;

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;.= (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

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;.= ((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