let i, j be Integer; :: thesis: for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
let G be Group; :: thesis: for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
let h be Element of G; :: thesis: h |^ (i + j) = (h |^ i) * (h |^ j)
defpred S₁[ Integer] means for i being Integer holds h |^ (i + $1) = (h |^ i) * (h |^ $1);
A1: 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 A2: for i being Integer holds h |^ (i + j) = (h |^ i) * (h |^ j) ; :: thesis: ( S₁[j - 1] & S₁[j + 1] )
thus for i being Integer holds h |^ (i + (j - 1)) = (h |^ i) * (h |^ (j - 1)) :: thesis: S₁[j + 1]

proof

let i be Integer; :: thesis: h |^ (i + (j - 1)) = (h |^ i) * (h |^ (j - 1))
thus h |^ (i + (j - 1)) = h |^ ((i - 1) + j)
.= (h |^ (i - 1)) * (h |^ j) by A2
.= ((h |^ i) * (h |^ (- 1))) * (h |^ j) by Lm14
.= (h |^ i) * ((h |^ (- 1)) * (h |^ j)) by Def3
.= (h |^ i) * (h |^ (j + (- 1))) by A2
.= (h |^ i) * (h |^ (j - 1)) ; :: thesis: verum

end;

let i be Integer; :: thesis: h |^ (i + (j + 1)) = (h |^ i) * (h |^ (j + 1))
thus h |^ (i + (j + 1)) = h |^ ((i + 1) + j)
.= (h |^ (i + 1)) * (h |^ j) by A2
.= ((h |^ i) * (h |^ 1)) * (h |^ j) by Lm16
.= (h |^ i) * ((h |^ 1) * (h |^ j)) by Def3
.= (h |^ i) * (h |^ (j + 1)) by A2 ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

let i be Integer; :: thesis: h |^ (i + 0) = (h |^ i) * (h |^ 0)
thus h |^ (i + 0) = (h |^ i) * (1_ G) by Def4
.= (h |^ i) * (h |^ 0) by Def7 ; :: thesis: verum

end;

for j being Integer holds S₁[j] from INT_1:sch 4(A3, A1);
hence h |^ (i + j) = (h |^ i) * (h |^ j) ; :: thesis: verum