let x be Real; :: thesis: for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m)
let m, n be Nat; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

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

suppose x <> 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

hence x #Z (n + m) = (x #Z n) * (x #Z m) by PREPOWER:44; :: thesis: verum

end;

suppose A1: x = 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

thus x #Z (n + m) = (x #Z n) * (x #Z m) :: thesis: verum

proof

A2: 0 #Z (n + m) = 0 |^ |.(n + m).| by PREPOWER:def 3
.= 0 |^ (n + m) by ABSVALUE:def 1
.= (0 |^ n) * (0 |^ m) by NEWTON:8 ;

per cases ( ( n = 0 & m = 0 ) or n <> 0 or m <> 0 ) ;

suppose A3: ( n = 0 & m = 0 ) ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

x #Z (0 + 0) = 1 * (x #Z 0)
.= (x #Z 0) * (x #Z 0) by PREPOWER:34 ;
hence x #Z (n + m) = (x #Z n) * (x #Z m) by A3; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

then A4: 0 + 1 <= n by NAT_1:13;
A5: (0 #Z n) * (0 #Z m) = (0 |^ |.n.|) * (0 #Z m) by PREPOWER:def 3
.= (0 |^ n) * (0 #Z m) by ABSVALUE:def 1
.= 0 * (0 #Z m) by A4, NEWTON:11 ;
0 #Z (n + m) = 0 * (0 |^ m) by A2, A4, NEWTON:11;
hence x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A5; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: x #Z (n + m) = (x #Z n) * (x #Z m)

then A6: 0 + 1 <= m by NAT_1:13;
A7: (0 #Z n) * (0 #Z m) = (0 |^ |.m.|) * (0 #Z n) by PREPOWER:def 3
.= (0 |^ m) * (0 #Z n) by ABSVALUE:def 1
.= 0 * (0 #Z n) by A6, NEWTON:11 ;
0 #Z (n + m) = 0 * (0 |^ n) by A2, A6, NEWTON:11;
hence x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A7; :: thesis: verum

end;

end;

end;

end;

end;