defpred S1[ Nat, Nat, Point of (TOP-REAL 2)] means ( [$1,$2] in [:(dom v1),(dom v2):] & ( for r, s being Real st v1 . $1 = r & v2 . $2 = s holds
$3 = |[r,s]| ) );
A2:
dom v1 = Seg (len v1)
by FINSEQ_1:def 3;
A3:
for i, j being Nat st [i,j] in [:(Seg (len v1)),(Seg (len v2)):] holds
ex p being Point of (TOP-REAL 2) st S1[i,j,p]
proof
let i,
j be
Nat;
( [i,j] in [:(Seg (len v1)),(Seg (len v2)):] implies ex p being Point of (TOP-REAL 2) st S1[i,j,p] )
assume A4:
[i,j] in [:(Seg (len v1)),(Seg (len v2)):]
;
ex p being Point of (TOP-REAL 2) st S1[i,j,p]
reconsider i9 =
i,
j9 =
j as
Element of
NAT by ORDINAL1:def 12;
reconsider s1 =
v1 . i9,
s2 =
v2 . j9 as
Real ;
take
|[s1,s2]|
;
S1[i,j,|[s1,s2]|]
thus
[i,j] in [:(dom v1),(dom v2):]
by A2, A4, FINSEQ_1:def 3;
for r, s being Real st v1 . i = r & v2 . j = s holds
|[s1,s2]| = |[r,s]|
let r,
s be
Real;
( v1 . i = r & v2 . j = s implies |[s1,s2]| = |[r,s]| )
assume
(
r = v1 . i &
s = v2 . j )
;
|[s1,s2]| = |[r,s]|
hence
|[s1,s2]| = |[r,s]|
;
verum
end;
consider M being Matrix of len v1, len v2, the carrier of (TOP-REAL 2) such that
A5:
for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)]
from MATRIX_0:sch 2(A3);
reconsider M = M as Matrix of the carrier of (TOP-REAL 2) ;
take
M
; ( len M = len v1 & width M = len v2 & ( for n, m being Nat st [n,m] in Indices M holds
M * (n,m) = |[(v1 . n),(v2 . m)]| ) )
thus
( len M = len v1 & width M = len v2 )
by A1, MATRIX_0:23; for n, m being Nat st [n,m] in Indices M holds
M * (n,m) = |[(v1 . n),(v2 . m)]|
let n, m be Nat; ( [n,m] in Indices M implies M * (n,m) = |[(v1 . n),(v2 . m)]| )
assume
[n,m] in Indices M
; M * (n,m) = |[(v1 . n),(v2 . m)]|
hence
M * (n,m) = |[(v1 . n),(v2 . m)]|
by A5; verum