let m, n be Nat; :: thesis: for D being non empty set
for l being Nat
for M being Matrix of n,m,D
for pD being FinSequence of D holds
( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )
let D be non empty set ; :: thesis: for l being Nat
for M being Matrix of n,m,D
for pD being FinSequence of D holds
( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )
let l be Nat; :: thesis: for M being Matrix of n,m,D
for pD being FinSequence of D holds
( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )
let M be Matrix of n,m,D; :: thesis: for pD being FinSequence of D holds
( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )
let pD be FinSequence of D; :: thesis: ( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )

now

per cases ( len pD = width M or len pD <> width M ) ;

case len pD = width M ; :: thesis: ( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )

then ( len M = len (ReplaceLine M,l,pD) & width M = width (RLine M,l,pD) ) by Def3;
hence ( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) ) by MATRIX_4:55; :: thesis: verum

end;

case len pD <> width M ; :: thesis: ( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) )

hence ( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) ) by Def3; :: thesis: verum

end;

end;

end;

hence ( Indices M = Indices (RLine M,l,pD) & len M = len (RLine M,l,pD) & width M = width (RLine M,l,pD) ) ; :: thesis: verum