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 p' being Element of D * st pD = p' holds
RLine M,l,pD = Replace M,l,p'
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 p' being Element of D * st pD = p' holds
RLine M,l,pD = Replace M,l,p'
let M be Matrix of n,m,D; :: thesis: for pD being FinSequence of D st len pD = width M holds
for p' being Element of D * st pD = p' holds
RLine M,l,pD = Replace M,l,p'
let pD be FinSequence of D; :: thesis: ( len pD = width M implies for p' being Element of D * st pD = p' holds
RLine M,l,pD = Replace M,l,p' )
assume A1: len pD = width M ; :: thesis: for p' being Element of D * st pD = p' holds
RLine M,l,pD = Replace M,l,p'
let p' be Element of D * ; :: thesis: ( pD = p' implies RLine M,l,pD = Replace M,l,p' )
assume A2: pD = p' ; :: thesis: RLine M,l,pD = Replace M,l,p'
set RL = RLine M,l,pD;
set R = Replace M,l,p';
A3: ( len (Replace M,l,p') = len M & len M = len (RLine M,l,pD) ) by Lm4, FINSEQ_7:7;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (Replace M,l,p') implies (Replace M,l,p') . i = (RLine M,l,pD) . i )
assume A4: ( 1 <= i & i <= len (Replace M,l,p') ) ; :: thesis: (Replace M,l,p') . i = (RLine M,l,pD) . i
i in NAT by ORDINAL1:def 13;
then i in Seg (len (Replace M,l,p')) by A4;
then A5: ( i in dom (Replace M,l,p') & i in dom M & i in Seg n & n = len M ) by A3, FINSEQ_1:def 3, MATRIX_1:def 3;

now

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

case i = l ; :: thesis: (Replace M,l,p') . i = (RLine M,l,pD) . i

then ( (Replace M,l,p') /. i = p' & (Replace M,l,p') /. i = (Replace M,l,p') . i & Line (RLine M,l,pD),i = pD & Line (RLine M,l,pD),i = (RLine M,l,pD) . i ) by A1, A3, A4, A5, Th28, FINSEQ_7:10, MATRIX_2:10, PARTFUN1:def 8;
hence (Replace M,l,p') . i = (RLine M,l,pD) . i by A2; :: thesis: verum

end;

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

then ( (Replace M,l,p') . i = (Replace M,l,p') /. i & (Replace M,l,p') /. i = M /. i & M /. i = M . i & M . i = Line M,i & Line M,i = Line (RLine M,l,pD),i & Line (RLine M,l,pD),i = (RLine M,l,pD) . i ) by A3, A4, A5, Th28, FINSEQ_7:12, MATRIX_2:10, PARTFUN1:def 8;
hence (Replace M,l,p') . i = (RLine M,l,pD) . i ; :: thesis: verum

end;

end;

end;

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

end;

hence RLine M,l,pD = Replace M,l,p' by A3, FINSEQ_1:18; :: thesis: verum