defpred S1[ Nat, Nat, Point of ()] 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 () st S1[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 () st S1[i,j,p] )
assume A4: [i,j] in [:(Seg (len v1)),(Seg (len v2)):] ; :: thesis: ex p being Point of () 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]| ; :: thesis: S1[i,j,|[s1,s2]|]
thus [i,j] in [:(dom v1),(dom v2):] by ; :: 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 () such that
A5: for i, j being Nat st [i,j] in Indices M holds
S1[i,j,M * (i,j)] from reconsider M = M as Matrix of the carrier of () ;
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 ; :: 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