let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₁,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 non-empty ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ^ ((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; :: thesis: ^ ((- (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; :: thesis: verum