defpred S4[ 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) & dom v2 = Seg (len v2) )
by FINSEQ_1:def 3;
A3:
for i, j being Nat st [i,j] in [:(Seg (len v1)),(Seg (len v2)):] holds
for p1, p2 being Point of (TOP-REAL 2) st S4[i,j,p1] & S4[i,j,p2] holds
p1 = p2
proof
let i,
j be
Nat;
:: thesis: ( [i,j] in [:(Seg (len v1)),(Seg (len v2)):] implies for p1, p2 being Point of (TOP-REAL 2) st S4[i,j,p1] & S4[i,j,p2] holds
p1 = p2 )
assume
[i,j] in [:(Seg (len v1)),(Seg (len v2)):]
;
:: thesis: for p1, p2 being Point of (TOP-REAL 2) st S4[i,j,p1] & S4[i,j,p2] holds
p1 = p2
reconsider i' =
i,
j' =
j as
Element of
NAT by ORDINAL1:def 13;
reconsider s1 =
v1 . i',
s2 =
v2 . j' as
Real ;
let p1,
p2 be
Point of
(TOP-REAL 2);
:: thesis: ( S4[i,j,p1] & S4[i,j,p2] implies p1 = p2 )
assume
(
S4[
i,
j,
p1] &
S4[
i,
j,
p2] )
;
:: thesis: p1 = p2
then
(
p1 = |[s1,s2]| &
p2 = |[s1,s2]| )
;
hence
p1 = p2
;
:: thesis: verum
end;
A4:
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 S4[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 S4[i,j,p] )
assume A5:
[i,j] in [:(Seg (len v1)),(Seg (len v2)):]
;
:: thesis: ex p being Point of (TOP-REAL 2) st S4[i,j,p]
reconsider i' =
i,
j' =
j as
Element of
NAT by ORDINAL1:def 13;
reconsider s1 =
v1 . i',
s2 =
v2 . j' as
Real ;
take
|[s1,s2]|
;
:: thesis: S4[i,j,|[s1,s2]|]
thus
[i,j] in [:(dom v1),(dom v2):]
by A2, A5;
:: 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
A6:
for i, j being Nat st [i,j] in Indices M holds
S4[i,j,M * i,j]
from MATRIX_1:sch 2(A3, A4);
( len v1 <> 0 & len v2 <> 0 )
by A1;
then A7:
( 0 < len v1 & 0 < len v2 )
;
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 Element of 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 A7, MATRIX_1:24; :: thesis: for n, m being Element of NAT st [n,m] in Indices M holds
M * n,m = |[(v1 . n),(v2 . m)]|
let n, m be Element of 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 A6; :: thesis: verum