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
A8: ( 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)]| ) ) and
A9: ( 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)]| ) ) ; :: thesis: G1 = G2
A10: ( Indices G1 = [:(dom G1),(Seg (width G1)):] & Indices G2 = [:(dom G2),(Seg (width G2)):] ) by MATRIX_1:def 5;

now

let n, m be Nat; :: thesis: ( [n,m] in Indices G1 implies G1 * n,m = G2 * n,m )
assume A11: [n,m] in Indices G1 ; :: thesis: G1 * n,m = G2 * n,m
reconsider m' = m, n' = n as Element of NAT by ORDINAL1:def 13;
A12: ( dom G1 = Seg (len G1) & dom G2 = Seg (len G2) ) by FINSEQ_1:def 3;
reconsider r = v1 . n', s = v2 . m' as Real ;
( G1 * n,m = |[r,s]| & G2 * n,m = |[r,s]| ) by A8, A9, A10, A11, A12;
hence G1 * n,m = G2 * n,m ; :: thesis: verum

end;

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