scheme :: MATRIX_0:sch 2
MatrixEx{ F₁() -> non empty set , F₂() -> Nat, F₃() -> Nat, P₁[ object , object , object ] } :

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)]

provided

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]