:: deftheorem defines Del PENCIL_2:def 1 :
for D being set
for p being FinSequence of D
for i, j being Nat holds Del (p,i,j) = (p | (i -' 1)) ^ (p /^ j);