let m, n, l 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:7;

A4: now

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
i in NAT by ORDINAL1:def 13;
then 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_1:def 3;
A10: i in dom M by A3, A7, FINSEQ_1:def 3;

now

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 8;
(Replace M,l,p9) /. i = p9 by A3, A5, A6, A11, FINSEQ_7:10;
hence (Replace M,l,p9) . i = (RLine M,l,pD) . i by A2, A9, A13, A12, MATRIX_2:10; :: 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 8;
A17: M . i = Line M,i by A9, MATRIX_2:10;
A18: M /. i = M . i by A10, PARTFUN1:def 8;
(Replace M,l,p9) /. i = M /. i by A3, A5, A6, A14, FINSEQ_7:12;
hence (Replace M,l,p9) . i = (RLine M,l,pD) . i by A9, A16, A18, A17, A15, MATRIX_2:10; :: 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:18, FINSEQ_7:7; :: thesis: verum