theorem
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 b2,
b1 -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
I being
integer SortSymbol of
S for
u being
ManySortedFunction of
FreeGen T, the
Sorts of
C for
t1,
t2 being
Element of
T,
I holds
(init.array (t1,t2)) value_at (
C,
u)
= init.array (
(t1 value_at (C,u)),
(t2 value_at (C,u)))