let L be Field; :: thesis: for m being Element of NAT st 0 < m holds
for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1
let m be Element of NAT ; :: thesis: ( 0 < m implies for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1 )
assume A1: m > 0 ; :: thesis: for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds
u * v = (emb (m,L)) * u1
let u, v, u1 be Matrix of m,L; :: thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) implies u * v = (emb (m,L)) * u1 )
assume A2: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ; :: thesis: u * v = (emb (m,L)) * u1
A3: for i, j being Nat st [i,j] in Indices (u * v) holds
(u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (u * v) implies (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) )
A4: ( [i,j] in Indices (u * v) implies ( 1 <= i & i <= m & 1 <= j & j <= m ) )

proof

width u = m by MATRIX_0:24
.= len v by MATRIX_0:24 ;
then A5: width (u * v) = width v by MATRIX_3:def 4
.= m by MATRIX_0:24 ;
assume A6: [i,j] in Indices (u * v) ; :: thesis: ( 1 <= i & i <= m & 1 <= j & j <= m )
then A7: j in Seg m by A5, ZFMISC_1:87;
width u = m by MATRIX_0:24
.= len v by MATRIX_0:24 ;
then len (u * v) = len u by MATRIX_3:def 4
.= m by MATRIX_0:24 ;
then u * v is Matrix of m,m,L by A1, A5, MATRIX_0:20;
then Indices (u * v) = [:(Seg m),(Seg m):] by A5, MATRIX_0:25;
then i in Seg m by A6, ZFMISC_1:87;
hence ( 1 <= i & i <= m & 1 <= j & j <= m ) by A7, FINSEQ_1:1; :: thesis: verum

end;

assume A8: [i,j] in Indices (u * v) ; :: thesis: (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j)
then ( i in Seg m & j in Seg m ) by A4;
then [i,j] in [:(Seg m),(Seg m):] by ZFMISC_1:87;
then [i,j] in Indices u1 by MATRIX_0:24;
then ((emb (m,L)) * u1) * (i,j) = (emb (m,L)) * (u1 * (i,j)) by MATRIX_3:def 5;
hence (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) by A2, A8, A4; :: thesis: verum

end;

A9: width ((emb (m,L)) * u1) = width u1 by MATRIX_3:def 5
.= m by MATRIX_0:24 ;
width u = m by MATRIX_0:24
.= len v by MATRIX_0:24 ;
then A10: width (u * v) = width v by MATRIX_3:def 4
.= m by MATRIX_0:24 ;
width u = m by MATRIX_0:24
.= len v by MATRIX_0:24 ;
then A11: len (u * v) = len u by MATRIX_3:def 4
.= m by MATRIX_0:24 ;
len ((emb (m,L)) * u1) = len u1 by MATRIX_3:def 5
.= m by MATRIX_0:24 ;
hence u * v = (emb (m,L)) * u1 by A11, A9, A10, A3, MATRIX_0:21; :: thesis: verum