defpred S_{1}[ 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_{1}[i,j,p]

A5: for i, j being Nat st [i,j] in Indices M holds

S_{1}[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

$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

proof

consider M being Matrix of len v1, len v2, the carrier of (TOP-REAL 2) such that
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_{1}[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_{1}[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_{1}[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;assume A4: [i,j] in [:(Seg (len v1)),(Seg (len v2)):] ; :: thesis: ex p being Point of (TOP-REAL 2) st S

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

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

A5: for i, j being Nat st [i,j] in Indices M holds

S

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