for X being set
for S being with_empty_element cap-closed Subset-Family of X
for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed V224() Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = SumAll Mx )