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 4
.= (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 4
.= (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) by VECTSP_1:def 13
.= (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