ex M being Matrix of F₂(),F₃(),F₁() st
for i, j being Nat st [i,j] in Indices M holds
P₁[i,j,M * (i,j)]

A1: for i, j being Nat st [i,j] in [:(Seg F₂()),(Seg F₃()):] holds
ex x being Element of F₁() st P₁[i,j,x]