theorem :: AOFA_A01:89

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 holds ^ (1,T,I) = (\0 (T,I)) + (\1 (T,I))