let S be 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)
let F1, F2 be 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)
defpred S1[ 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 S1[i,j,K]
proof
let i,
j be
Nat;
( [i,j] in [:(Seg (len F1)),(Seg (len F2)):] implies ex K being Element of S st S1[i,j,K] )
assume
[i,j] in [:(Seg (len F1)),(Seg (len F2)):]
;
ex K being Element of S st S1[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
S1[
i,
j,
K]
;
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
S1[i,j,Mx * (i,j)]
from MATRIX_0:sch 2(A2);
take
Mx
; 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; verum