reconsider Mf = M * F as Matrix of n,m,D by Lm7;
let Mp be Matrix of n,m,D; :: thesis: ( Mp = F * M iff ( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) ) )
thus ( Mp = M * F implies ( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) ) ) :: thesis: ( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) implies Mp = F * M )

proof

A1: rng F c= Seg n by RELAT_1:def 19;
assume A2: Mp = M * F ; :: thesis: ( len Mp = len M & width Mp = width M & ( for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ) )
A3: len M = n by MATRIX_0:def 2;
A4: len Mp = n by MATRIX_0:def 2;

A5: now :: thesis: ( ( n = 0 & width M = width Mp ) or ( n > 0 & width M = width Mp ) )

per cases ( n = 0 or n > 0 ) ;

case A6: n = 0 ; :: thesis: width M = width Mp

then width M = 0 by A3, MATRIX_0:def 3;
hence width M = width Mp by A4, A6, MATRIX_0:def 3; :: thesis: verum

end;

case A7: n > 0 ; :: thesis: width M = width Mp

then width M = m by A3, MATRIX_0:20;
hence width M = width Mp by A4, A7, MATRIX_0:20; :: thesis: verum

end;

end;

end;

hence ( len Mp = len M & width Mp = width M ) by A3, MATRIX_0:def 2; :: thesis: for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j)
let i, j, k be Nat; :: thesis: ( [i,j] in Indices M & F . i = k implies Mp * (i,j) = M * (k,j) )
assume that
A8: [i,j] in Indices M and
A9: F . i = k ; :: thesis: Mp * (i,j) = M * (k,j)
Indices M = [:(Seg n),(Seg (width M)):] by MATRIX_0:25;
then A10: i in Seg n by A8, ZFMISC_1:87;
then A11: Line (Mp,i) = Mp . i by MATRIX_0:52;
dom F = Seg n by FUNCT_2:52;
then A12: F . i in rng F by A10, FUNCT_1:def 3;
len Mp = n by MATRIX_0:25;
then dom Mp = Seg n by FINSEQ_1:def 3;
then Mp . i = M . k by A2, A9, A10, FUNCT_1:12;
then A13: Line (Mp,i) = Line (M,k) by A9, A12, A1, A11, MATRIX_0:52;
A14: j in Seg (width M) by A8, ZFMISC_1:87;
then (Line (M,k)) . j = M * (k,j) by MATRIX_0:def 7;
hence Mp * (i,j) = M * (k,j) by A5, A14, A13, MATRIX_0:def 7; :: thesis: verum

end;

assume that
A15: len Mp = len M and
A16: width Mp = width M ; :: thesis: ( ex i, j, k being Nat st
( [i,j] in Indices M & F . i = k & not Mp * (i,j) = M * (k,j) ) or Mp = F * M )
assume A17: for i, j, k being Nat st [i,j] in Indices M & F . i = k holds
Mp * (i,j) = M * (k,j) ; :: thesis: Mp = F * M
for i, j being Nat st [i,j] in Indices Mp holds
Mp * (i,j) = Mf * (i,j)

proof

A18: Indices Mp = Indices M by A15, A16, MATRIX_4:55;
let i, j be Nat; :: thesis: ( [i,j] in Indices Mp implies Mp * (i,j) = Mf * (i,j) )
assume A19: [i,j] in Indices Mp ; :: thesis: Mp * (i,j) = Mf * (i,j)
Indices Mp = [:(Seg n),(Seg (width M)):] by A16, MATRIX_0:25;
then A20: i in Seg n by A19, ZFMISC_1:87;
then A21: Line (Mf,i) = Mf . i by MATRIX_0:52;
A22: rng F c= Seg n by RELAT_1:def 19;
dom F = Seg n by FUNCT_2:52;
then A23: F . i in rng F by A20, FUNCT_1:def 3;
then F . i in Seg n by A22;
then reconsider k = F . i as Element of NAT ;
len Mf = n by MATRIX_0:25;
then dom Mf = Seg n by FINSEQ_1:def 3;
then Mf . i = M . k by A20, FUNCT_1:12;
then A24: Line (Mf,i) = Line (M,k) by A23, A22, A21, MATRIX_0:52;
A25: width M = len (Line (M,k)) by MATRIX_0:def 7;
A26: width Mf = len (Line (Mf,i)) by MATRIX_0:def 7;
A27: j in Seg (width M) by A16, A19, ZFMISC_1:87;
then (Line (M,k)) . j = M * (k,j) by MATRIX_0:def 7;
then Mf * (i,j) = M * (k,j) by A27, A24, A25, A26, MATRIX_0:def 7;
hence Mp * (i,j) = Mf * (i,j) by A17, A19, A18; :: thesis: verum

end;

hence Mp = F * M by MATRIX_0:27; :: thesis: verum