let G1, G2 be Matrix of (TOP-REAL 2); :: thesis: ( 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)]| ; :: thesis: G1 = G2
A10: ( Indices G1 = [:(dom G1),(Seg (width G1)):] & Indices G2 = [:(dom G2),(Seg (width G2)):] ) by MATRIX_0:def 4;

now :: thesis: for n, m being Nat st [n,m] in Indices G1 holds
G1 * (n,m) = G2 * (n,m)

let n, m be Nat; :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum

end;

hence G1 = G2 by A6, A8, MATRIX_0:21; :: thesis: verum