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_1:def 3;
A4: len Mp = n by MATRIX_1:def 3;

A5: now

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

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

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

end;

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

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

end;

end;

end;

hence ( len Mp = len M & width Mp = width M ) by A3, MATRIX_1:def 3; :: 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_1:26;
then A10: i in Seg n by A8, ZFMISC_1:106;
then A11: Line Mp,i = Mp . i by MATRIX_2:10;
dom F = Seg n by FUNCT_2:67;
then A12: F . i in rng F by A10, FUNCT_1:def 5;
len Mp = n by MATRIX_1:26;
then dom Mp = Seg n by FINSEQ_1:def 3;
then Mp . i = M . k by A2, A9, A10, FUNCT_1:22;
then A13: Line Mp,i = Line M,k by A9, A12, A1, A11, MATRIX_2:10;
A14: j in Seg (width M) by A8, ZFMISC_1:106;
then (Line M,k) . j = M * k,j by MATRIX_1:def 8;
hence Mp * i,j = M * k,j by A5, A14, A13, MATRIX_1:def 8; :: 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_1:26;
then A20: i in Seg n by A19, ZFMISC_1:106;
then A21: Line Mf,i = Mf . i by MATRIX_2:10;
A22: rng F c= Seg n by RELAT_1:def 19;
dom F = Seg n by FUNCT_2:67;
then A23: F . i in rng F by A20, FUNCT_1:def 5;
then F . i in Seg n by A22;
then reconsider k = F . i as Element of NAT ;
len Mf = n by MATRIX_1:26;
then dom Mf = Seg n by FINSEQ_1:def 3;
then Mf . i = M . k by A20, FUNCT_1:22;
then A24: Line Mf,i = Line M,k by A23, A22, A21, MATRIX_2:10;
A25: width M = len (Line M,k) by MATRIX_1:def 8;
A26: width Mf = len (Line Mf,i) by MATRIX_1:def 8;
A27: j in Seg (width M) by A16, A19, ZFMISC_1:106;
then (Line M,k) . j = M * k,j by MATRIX_1:def 8;
then Mf * i,j = M * k,j by A27, A24, A25, A26, MATRIX_1:def 8;
hence Mp * i,j = Mf * i,j by A17, A19, A18; :: thesis: verum

end;

hence Mp = F * M by MATRIX_1:28; :: thesis: verum