let N, M be Matrix of COMPLEX; :: thesis: ( len N = len M & width N = width M & ( for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = (M * (i,j)) *' ) implies ( len M = len N & width M = width N & ( for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *' ) ) )
assume that
A14: len N = len M and
A15: width N = width M and
A16: for i, j being Nat st [i,j] in Indices M holds
N * (i,j) = (M * (i,j)) *' ; :: thesis: ( len M = len N & width M = width N & ( for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *' ) )
thus len M = len N by A14; :: thesis: ( width M = width N & ( for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *' ) )
thus width M = width N by A15; :: thesis: for i, j being Nat st [i,j] in Indices N holds
M * (i,j) = (N * (i,j)) *'
let i, j be Nat; :: thesis: ( [i,j] in Indices N implies M * (i,j) = (N * (i,j)) *' )
assume A17: [i,j] in Indices N ; :: thesis: M * (i,j) = (N * (i,j)) *'
( 1 <= i & i <= len M & 1 <= j & j <= width M ) by A14, A15, A17, MATRIX_0:32;
then A18: [i,j] in Indices M by MATRIX_0:30;
thus M * (i,j) = ((M * (i,j)) *') *'
.= (N * (i,j)) *' by A18, A16 ; :: thesis: verum