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

assume A1: 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 ) )
A2: ( len M = n & len Mp = n ) by MATRIX_1:def 3;

A3: now

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

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

then ( width M = 0 & width Mp = 0 ) by A2, MATRIX_1:def 4;
hence width M = width Mp ; :: thesis: verum

end;

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

then ( width M = m & width Mp = m ) by A2, MATRIX_1:20;
hence width M = width Mp ; :: thesis: verum

end;

end;

end;

hence ( len Mp = len M & width Mp = width M ) by A2; :: 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 A4: ( [i,j] in Indices M & F . i = k ) ; :: thesis: Mp * i,j = M * k,j
( Indices M = [:(Seg n),(Seg (width M)):] & len Mp = n ) by MATRIX_1:26;
then A5: ( i in Seg n & j in Seg (width M) & dom F = Seg n & dom Mp = Seg n ) by A4, FINSEQ_1:def 3, FUNCT_2:67, ZFMISC_1:106;
then ( F . i in rng F & rng F c= Seg n ) by FUNCT_1:def 5, RELAT_1:def 19;
then ( Mp . i = M . k & Line Mp,i = Mp . i & k in Seg n ) by A1, A4, A5, FUNCT_1:22, MATRIX_2:10;
then ( Line Mp,i = Line M,k & (Line M,k) . j = M * k,j ) by A5, MATRIX_1:def 8, MATRIX_2:10;
hence Mp * i,j = M * k,j by A3, A5, MATRIX_1:def 8; :: thesis: verum

end;

assume A6: ( len Mp = len M & 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 A7: 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
reconsider Mf = M * F as Matrix of n,m,D by Lm7;
for i, j being Nat st [i,j] in Indices Mp holds
Mp * i,j = Mf * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices Mp implies Mp * i,j = Mf * i,j )
assume A8: [i,j] in Indices Mp ; :: thesis: Mp * i,j = Mf * i,j
( Indices Mp = [:(Seg n),(Seg (width M)):] & len Mf = n ) by A6, MATRIX_1:26;
then A9: ( i in Seg n & j in Seg (width M) & dom F = Seg n & dom Mf = Seg n ) by A8, FINSEQ_1:def 3, FUNCT_2:67, ZFMISC_1:106;
then A10: ( F . i in rng F & rng F c= Seg n ) by FUNCT_1:def 5, RELAT_1:def 19;
then F . i in Seg n ;
then reconsider k = F . i as Element of NAT ;
( Mf . i = M . k & Line Mf,i = Mf . i & k in Seg n ) by A9, A10, FUNCT_1:22, MATRIX_2:10;
then ( Line Mf,i = Line M,k & (Line M,k) . j = M * k,j & width M = len (Line M,k) & width Mf = len (Line Mf,i) ) by A9, MATRIX_1:def 8, MATRIX_2:10;
then ( Mf * i,j = M * k,j & Indices Mp = Indices M ) by A6, A9, MATRIX_1:def 8, MATRIX_4:55;
hence Mp * i,j = Mf * i,j by A7, A8; :: thesis: verum

end;

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