let l, n, m be Nat; :: thesis: for D being non empty set
for M being Matrix of n,m,D
for pD being FinSequence of D st len pD = width M holds
for p9 being Element of D * st pD = p9 holds
RLine (M,l,pD) = Replace (M,l,p9)
let D be non empty set ; :: thesis: for M being Matrix of n,m,D
for pD being FinSequence of D st len pD = width M holds
for p9 being Element of D * st pD = p9 holds
RLine (M,l,pD) = Replace (M,l,p9)
let M be Matrix of n,m,D; :: thesis: for pD being FinSequence of D st len pD = width M holds
for p9 being Element of D * st pD = p9 holds
RLine (M,l,pD) = Replace (M,l,p9)
let pD be FinSequence of D; :: thesis: ( len pD = width M implies for p9 being Element of D * st pD = p9 holds
RLine (M,l,pD) = Replace (M,l,p9) )
assume A1: len pD = width M ; :: thesis: for p9 being Element of D * st pD = p9 holds
RLine (M,l,pD) = Replace (M,l,p9)
set RL = RLine (M,l,pD);
let p9 be Element of D * ; :: thesis: ( pD = p9 implies RLine (M,l,pD) = Replace (M,l,p9) )
assume A2: pD = p9 ; :: thesis: RLine (M,l,pD) = Replace (M,l,p9)
set R = Replace (M,l,p9);
A3: len (Replace (M,l,p9)) = len M by FINSEQ_7:5;

A4: now :: thesis: for i being Nat st 1 <= i & i <= len (Replace (M,l,p9)) holds
(Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (Replace (M,l,p9)) implies (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i )
assume that
A5: 1 <= i and
A6: i <= len (Replace (M,l,p9)) ; :: thesis: (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i
A7: i in Seg (len (Replace (M,l,p9))) by A5, A6;
then A8: i in dom (Replace (M,l,p9)) by FINSEQ_1:def 3;
A9: i in Seg n by A3, A7, MATRIX_0:def 2;
A10: i in dom M by A3, A7, FINSEQ_1:def 3;

now :: thesis: ( ( i = l & (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i ) or ( i <> l & (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i ) )

per cases ( i = l or i <> l ) ;

case A11: i = l ; :: thesis: (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i

then A12: Line ((RLine (M,l,pD)),i) = pD by A1, A9, Th28;
A13: (Replace (M,l,p9)) /. i = (Replace (M,l,p9)) . i by A8, PARTFUN1:def 6;
(Replace (M,l,p9)) /. i = p9 by A3, A5, A6, A11, FINSEQ_7:8;
hence (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i by A2, A9, A13, A12, MATRIX_0:52; :: thesis: verum

end;

case A14: i <> l ; :: thesis: (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i

then A15: Line (M,i) = Line ((RLine (M,l,pD)),i) by A9, Th28;
A16: (Replace (M,l,p9)) . i = (Replace (M,l,p9)) /. i by A8, PARTFUN1:def 6;
A17: M . i = Line (M,i) by A9, MATRIX_0:52;
A18: M /. i = M . i by A10, PARTFUN1:def 6;
(Replace (M,l,p9)) /. i = M /. i by A3, A5, A6, A14, FINSEQ_7:10;
hence (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i by A9, A16, A18, A17, A15, MATRIX_0:52; :: thesis: verum

end;

end;

end;

hence (Replace (M,l,p9)) . i = (RLine (M,l,pD)) . i ; :: thesis: verum

end;

len M = len (RLine (M,l,pD)) by Lm4;
hence RLine (M,l,pD) = Replace (M,l,p9) by A4, FINSEQ_1:14, FINSEQ_7:5; :: thesis: verum