let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being non-empty b1,S -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)) )
let X be V3() ManySortedSet of the carrier of S; for T being non-empty X,S -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)) )
let T be non-empty X,S -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)) )
let I be 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)) )
let n be Nat; ( ^ ((n + 1),T,I) = (^ (n,T,I)) + (\1 (T,I)) & ^ ((- (n + 1)),T,I) = - (^ ((n + 1),T,I)) )
consider f being Function of INT,( the Sorts of T . I) such that
A1:
( ^ ((n + 1),T,I) = f . (n + 1) & f . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st f . j = t holds
( f . (j + 1) = t + (\1 (T,I)) & f . (- (j + 1)) = - (t + (\1 (T,I))) ) ) )
by Def15;
consider g being Function of INT,( the Sorts of T . I) such that
A2:
( ^ (n,T,I) = g . n & g . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st g . j = t holds
( g . (j + 1) = t + (\1 (T,I)) & g . (- (j + 1)) = - (t + (\1 (T,I))) ) ) )
by Def15;
consider h being Function of INT,( the Sorts of T . I) such that
A3:
( ^ ((- (n + 1)),T,I) = h . (- (n + 1)) & h . 0 = \0 (T,I) & ( for j being Nat
for t being Element of T,I st h . j = t holds
( h . (j + 1) = t + (\1 (T,I)) & h . (- (j + 1)) = - (t + (\1 (T,I))) ) ) )
by Def15;
A4:
f = g
by A1, A2, Lm1;
^ (n,T,I) = f . n
by A1, A2, Lm1;
hence A5:
^ ((n + 1),T,I) = (^ (n,T,I)) + (\1 (T,I))
by A1; ^ ((- (n + 1)),T,I) = - (^ ((n + 1),T,I))
f = h
by A1, A3, Lm1;
hence
^ ((- (n + 1)),T,I) = - (^ ((n + 1),T,I))
by A3, A5, A4, A2; verum