let G1, G2 be Matrix of (TOP-REAL 2); :: thesis: ( len G1 = len v1 & width G1 = len v2 & ( for n, m being Element of 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 Element of NAT st [n,m] in Indices G2 holds
G2 * (n,m) = |[(v1 . n),(v2 . m)]| ) implies G1 = G2 )
assume that
A9: ( len G1 = len v1 & width G1 = len v2 ) and
A10: for n, m being Element of NAT st [n,m] in Indices G1 holds
G1 * (n,m) = |[(v1 . n),(v2 . m)]| and
A11: ( len G2 = len v1 & width G2 = len v2 ) and
A12: for n, m being Element of NAT st [n,m] in Indices G2 holds
G2 * (n,m) = |[(v1 . n),(v2 . m)]| ; :: thesis: G1 = G2
A13: ( Indices G1 = [:(dom G1),(Seg (width G1)):] & Indices G2 = [:(dom G2),(Seg (width G2)):] ) by MATRIX_1:def 4;

now

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;
A14: ( 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 A15: [n,m] in Indices G1 ; :: thesis: G1 * (n,m) = G2 * (n,m)
then G1 * (n,m) = |[r,s]| by A10;
hence G1 * (n,m) = G2 * (n,m) by A9, A11, A12, A13, A15, A14; :: thesis: verum

end;

hence G1 = G2 by A9, A11, MATRIX_1:21; :: thesis: verum