let S be non empty cap-closed set ; :: thesis: 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)
let F1, F2 be FinSequence of S; :: thesis: 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)
defpred S₁[ Nat, Nat, set ] means $3 = (F1 . $1) /\ (F2 . $2);
A2: for i, j being Nat st [i,j] in [:(Seg (len F1)),(Seg (len F2)):] holds
ex K being Element of S st S₁[i,j,K]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (len F1)),(Seg (len F2)):] implies ex K being Element of S st S₁[i,j,K] )
assume [i,j] in [:(Seg (len F1)),(Seg (len F2)):] ; :: thesis: ex K being Element of S st S₁[i,j,K]
then ( i in Seg (len F1) & j in Seg (len F2) ) by ZFMISC_1:87;
then ( i in dom F1 & j in dom F2 ) by FINSEQ_1:def 3;
then ( F1 . i in rng F1 & F2 . j in rng F2 ) by FUNCT_1:3;
then (F1 . i) /\ (F2 . j) in S by FINSUB_1:def 2;
hence ex K being Element of S st S₁[i,j,K] ; :: thesis: verum

end;

consider Mx being Matrix of len F1, len F2,S such that
A3: for i, j being Nat st [i,j] in Indices Mx holds
S₁[i,j,Mx * (i,j)] from MATRIX_0:sch 2(A2);
take Mx ; :: thesis: for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = (F1 . i) /\ (F2 . j)
thus for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = (F1 . i) /\ (F2 . j) by A3; :: thesis: verum