let L be Field; for i, j being Integer
for x being Element of L st x <> 0. L holds
(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
let i, j be Integer; for x being Element of L st x <> 0. L holds
(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
let x be Element of L; ( x <> 0. L implies (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) )
defpred S1[ Integer] means for i being Integer holds pow (x,(i + $1)) = (pow (x,i)) * (pow (x,$1));
assume A1:
x <> 0. L
; (pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
A2:
for j being Integer st S1[j] holds
( S1[j - 1] & S1[j + 1] )
proof
let j be
Integer;
( S1[j] implies ( S1[j - 1] & S1[j + 1] ) )
assume A3:
for
i being
Integer holds
pow (
x,
(i + j))
= (pow (x,i)) * (pow (x,j))
;
( S1[j - 1] & S1[j + 1] )
thus
for
i being
Integer holds
pow (
x,
(i + (j - 1)))
= (pow (x,i)) * (pow (x,(j - 1)))
S1[j + 1]proof
let i be
Integer;
pow (x,(i + (j - 1))) = (pow (x,i)) * (pow (x,(j - 1)))
thus pow (
x,
(i + (j - 1))) =
pow (
x,
((i - 1) + j))
.=
(pow (x,(i - 1))) * (pow (x,j))
by A3
.=
((pow (x,i)) * (pow (x,(- 1)))) * (pow (x,j))
by A1, Th20
.=
(pow (x,i)) * ((pow (x,(- 1))) * (pow (x,j)))
by GROUP_1:def 3
.=
(pow (x,i)) * (pow (x,(j + (- 1))))
by A3
.=
(pow (x,i)) * (pow (x,(j - 1)))
;
verum
end;
let i be
Integer;
pow (x,(i + (j + 1))) = (pow (x,i)) * (pow (x,(j + 1)))
thus pow (
x,
(i + (j + 1))) =
pow (
x,
((i + 1) + j))
.=
(pow (x,(i + 1))) * (pow (x,j))
by A3
.=
((pow (x,i)) * (pow (x,1))) * (pow (x,j))
by A1, Th19
.=
(pow (x,i)) * ((pow (x,1)) * (pow (x,j)))
by GROUP_1:def 3
.=
(pow (x,i)) * (pow (x,(j + 1)))
by A3
;
verum
end;
A4:
S1[ 0 ]
for j being Integer holds S1[j]
from INT_1:sch 4(A4, A2);
hence
(pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
; verum