let L be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( x <> 0. L implies (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) )
defpred S₁[ Integer] means for i being Integer holds pow (x,(i + $1)) = (pow (x,i)) * (pow (x,$1));
assume A1: x <> 0. L ; :: thesis: (pow (x,i)) * (pow (x,j)) = pow (x,(i + j))
A2: for j being Integer st S₁[j] holds
( S₁[j - 1] & S₁[j + 1] )

proof

let j be Integer; :: thesis: ( S₁[j] implies ( S₁[j - 1] & S₁[j + 1] ) )
assume A3: for i being Integer holds pow (x,(i + j)) = (pow (x,i)) * (pow (x,j)) ; :: thesis: ( S₁[j - 1] & S₁[j + 1] )
thus for i being Integer holds pow (x,(i + (j - 1))) = (pow (x,i)) * (pow (x,(j - 1))) :: thesis: S₁[j + 1]

proof

let i be Integer; :: thesis: 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))) ; :: thesis: verum

end;

let i be Integer; :: thesis: 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 ; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

let i be Integer; :: thesis: pow (x,(i + 0)) = (pow (x,i)) * (pow (x,0))
thus pow (x,(i + 0)) = (pow (x,i)) * (1. L)
.= (pow (x,i)) * (pow (x,0)) by Th13 ; :: thesis: verum

end;

for j being Integer holds S₁[j] from INT_1:sch 4(A4, A2);
hence (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) ; :: thesis: verum