let n, m 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 :: thesis: ( ( len pD = width M & Indices M = Indices (RLine (M,l,pD)) & len M = len (RLine (M,l,pD)) & width M = width (RLine (M,l,pD)) ) or ( len pD <> width M & Indices M = Indices (RLine (M,l,pD)) & len M = len (RLine (M,l,pD)) & width M = width (RLine (M,l,pD)) ) )

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

case A1: 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 A2: width M = width (RLine (M,l,pD)) by Def3;
len M = len (ReplaceLine (M,l,pD)) by A1, Def3;
hence ( Indices M = Indices (RLine (M,l,pD)) & len M = len (RLine (M,l,pD)) & width M = width (RLine (M,l,pD)) ) by A2, 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