scheme :: MATRIX_0:sch 1
MatrixLambda{ F1() -> non empty set , F2() -> Nat, F3() -> Nat, F4( set , set ) -> Element of F1() } :
ex M being Matrix of F2(),F3(),F1() st
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = F4(i,j)