defpred S₁[ 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 S₁[i,j,p]

proof

let i, j be Nat; :: thesis: ( [i,j] in [:(Seg (len v1)),(Seg (len v2)):] implies ex p being Point of (TOP-REAL 2) st S₁[i,j,p] )
assume A4: [i,j] in [:(Seg (len v1)),(Seg (len v2)):] ; :: thesis: ex p being Point of (TOP-REAL 2) st S₁[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]| ; :: thesis: S₁[i,j,|[s1,s2]|]
thus [i,j] in [:(dom v1),(dom v2):] by A2, A4, FINSEQ_1:def 3; :: thesis: for r, s being Real st v1 . i = r & v2 . j = s holds
|[s1,s2]| = |[r,s]|
let r, s be Real; :: thesis: ( v1 . i = r & v2 . j = s implies |[s1,s2]| = |[r,s]| )
assume ( r = v1 . i & s = v2 . j ) ; :: thesis: |[s1,s2]| = |[r,s]|
hence |[s1,s2]| = |[r,s]| ; :: thesis: 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
S₁[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 ; :: thesis: ( 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; :: thesis: for n, m being Nat st [n,m] in Indices M holds
M * (n,m) = |[(v1 . n),(v2 . m)]|
let n, m be Nat; :: thesis: ( [n,m] in Indices M implies M * (n,m) = |[(v1 . n),(v2 . m)]| )
assume [n,m] in Indices M ; :: thesis: M * (n,m) = |[(v1 . n),(v2 . m)]|
hence M * (n,m) = |[(v1 . n),(v2 . m)]| by A5; :: thesis: verum