let G1, G2 be Matrix of (TOP-REAL 2); ( len G1 = len v1 & width G1 = len v2 & ( for n, m being Nat st [n,m] in Indices G1 holds
G1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len G2 = len v1 & width G2 = len v2 & ( for n, m being Nat st [n,m] in Indices G2 holds
G2 * (n,m) = |[(v1 . n),(v2 . m)]| ) implies G1 = G2 )
assume that
A6:
( len G1 = len v1 & width G1 = len v2 )
and
A7:
for n, m being Nat st [n,m] in Indices G1 holds
G1 * (n,m) = |[(v1 . n),(v2 . m)]|
and
A8:
( len G2 = len v1 & width G2 = len v2 )
and
A9:
for n, m being Nat st [n,m] in Indices G2 holds
G2 * (n,m) = |[(v1 . n),(v2 . m)]|
; G1 = G2
A10:
( Indices G1 = [:(dom G1),(Seg (width G1)):] & Indices G2 = [:(dom G2),(Seg (width G2)):] )
by MATRIX_0:def 4;
now for n, m being Nat st [n,m] in Indices G1 holds
G1 * (n,m) = G2 * (n,m)let n,
m be
Nat;
( [n,m] in Indices G1 implies G1 * (n,m) = G2 * (n,m) )reconsider m9 =
m,
n9 =
n as
Element of
NAT by ORDINAL1:def 12;
A11:
(
dom G1 = Seg (len G1) &
dom G2 = Seg (len G2) )
by FINSEQ_1:def 3;
reconsider r =
v1 . n9,
s =
v2 . m9 as
Real ;
assume A12:
[n,m] in Indices G1
;
G1 * (n,m) = G2 * (n,m)then
G1 * (
n,
m)
= |[r,s]|
by A7;
hence
G1 * (
n,
m)
= G2 * (
n,
m)
by A6, A8, A9, A10, A12, A11;
verum end;
hence
G1 = G2
by A6, A8, MATRIX_0:21; verum