:: deftheorem defines +* AOFA_A00:def 2 :
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for i being set st i in I holds
for j being set st j in A . i holds
for v being set st v in B . i holds
for b₈ being ManySortedFunction of A,B holds
( b₈ = F +* (i,j,v) iff ( b₈ . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
b₈ . s = F . s ) ) );