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 C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G
for i being Integer holds (^ (i,T,I)) value_at (C,s) = 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 C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G
for i being Integer holds (^ (i,T,I)) value_at (C,s) = 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 C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G
for i being Integer holds (^ (i,T,I)) value_at (C,s) = i
let C be bool-correct 4,1 integer 11,1,1 -array image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G
for i being Integer holds (^ (i,T,I)) value_at (C,s) = i
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for s being Element of C -States the generators of G
for i being Integer holds (^ (i,T,I)) value_at (C,s) = i
let I be integer SortSymbol of S; :: thesis: for s being Element of C -States the generators of G
for i being Integer holds (^ (i,T,I)) value_at (C,s) = i
let s be Element of C -States the generators of G; :: thesis: for i being Integer holds (^ (i,T,I)) value_at (C,s) = i
let i be Integer; :: thesis: (^ (i,T,I)) value_at (C,s) = i
defpred S₁[ Nat] means (^ ($1,T,I)) value_at (C,s) = $1;
^ (0,T,I) = \0 (T,I) by Th87;
then A1: S₁[ 0 ] by Th36;

A2: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
A4: (\1 (T,I)) value_at (C,s) = 1 by Th37;
^ ((i + 1),T,I) = (^ (i,T,I)) + (\1 (T,I)) by Th88;
then (^ ((i + 1),T,I)) value_at (C,s) = ((^ (i,T,I)) value_at (C,s)) + ((\1 (T,I)) value_at (C,s)) by Th39
.= ((^ (i,T,I)) value_at (C,s)) + 1 by A4, AOFA_A00:55 ;
hence S₁[i + 1] by A3; :: thesis: verum

end;

A5: for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
i in INT by INT_1:def 2;
then consider n being Nat such that
A6: ( i = n or i = - n ) by INT_1:def 1;

per cases ( i = n or ( i = - n & n = 0 ) or ( i = - n & n <> 0 ) ) by A6;

suppose ( i = n or ( i = - n & n = 0 ) ) ; :: thesis: (^ (i,T,I)) value_at (C,s) = i

hence (^ (i,T,I)) value_at (C,s) = i by A5; :: thesis: verum

end;

suppose A7: ( i = - n & n <> 0 ) ; :: thesis: (^ (i,T,I)) value_at (C,s) = i

then consider m being Nat such that
A8: n = m + 1 by NAT_1:6;
( (\1 (T,I)) value_at (C,s) = 1 & (^ (m,T,I)) value_at (C,s) = m ) by A5, Th37;
then A9: ((^ (m,T,I)) value_at (C,s)) + ((\1 (T,I)) value_at (C,s)) = m + 1 by AOFA_A00:55;
^ (i,T,I) = - (^ ((m + 1),T,I)) by A7, A8, Th88;
hence (^ (i,T,I)) value_at (C,s) = - ((^ ((m + 1),T,I)) value_at (C,s)) by Th38
.= - (((^ (m,T,I)) + (\1 (T,I))) value_at (C,s)) by Th88
.= - (((^ (m,T,I)) value_at (C,s)) + ((\1 (T,I)) value_at (C,s))) by Th39
.= i by A7, A8, A9, AOFA_A00:55 ;
:: thesis: verum

end;

end;