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;

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)

hence
G1 = G2
by A6, A8, MATRIX_0:21; :: thesis: verumG1 * (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;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