theorem Th88: :: AOFA_A01:88

for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for I being integer SortSymbol of S
for n being Nat holds
( ^ ((n + 1),T,I) = (^ (n,T,I)) + (\1 (T,I)) & ^ ((- (n + 1)),T,I) = - (^ ((n + 1),T,I)) )