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)

.= 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

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

A9: width ((emb (m,L)) * u1) =
width u1
by MATRIX_3:def 5
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 ) )

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;A4: ( [i,j] in Indices (u * v) implies ( 1 <= i & i <= m & 1 <= j & j <= m ) )

proof

assume A8:
[i,j] in Indices (u * v)
; :: thesis: (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j)
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;.= 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

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

.= 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