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 V3() 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 holds ^ (0,T,I) = \0 (T,I)
let X be V3() 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 holds ^ (0,T,I) = \0 (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 holds ^ (0,T,I) = \0 (T,I)
let I be integer SortSymbol of S; :: thesis: ^ (0,T,I) = \0 (T,I)
ex f being Function of INT,( the Sorts of T . I) st
( ^ (0,T,I) = f . 0 & 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;
hence ^ (0,T,I) = \0 (T,I) ; :: thesis: verum