for S being non empty cap-closed set
for F1, F2 being FinSequence of S ex Mx being Matrix of len F1, len F2,S st
for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = (F1 . i) /\ (F2 . j)