let n, m, k, i be Nat; :: thesis: for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for pA, pB being FinSequence of D st len pA = width A & len pB = width B holds
ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)
let D be non empty set ; :: thesis: for A being Matrix of n,m,D
for B being Matrix of n,k,D
for pA, pB being FinSequence of D st len pA = width A & len pB = width B holds
ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)
let A be Matrix of n,m,D; :: thesis: for B being Matrix of n,k,D
for pA, pB being FinSequence of D st len pA = width A & len pB = width B holds
ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)
let B be Matrix of n,k,D; :: thesis: for pA, pB being FinSequence of D st len pA = width A & len pB = width B holds
ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)
let pA, pB be FinSequence of D; :: thesis: ( len pA = width A & len pB = width B implies ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB) )
assume A1: ( len pA = width A & len pB = width B ) ; :: thesis: ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)
set AB = A ^^ B;
set RAB = RLine (A ^^ B),i,(pA ^ pB);
set RA = RLine A,i,pA;
set RB = RLine B,i,pB;
set Rab = (RLine A,i,pA) ^^ (RLine B,i,pB);
A2: ( len (RLine (A ^^ B),i,(pA ^ pB)) = n & len ((RLine A,i,pA) ^^ (RLine B,i,pB)) = n & dom (RLine (A ^^ B),i,(pA ^ pB)) = Seg (len (RLine (A ^^ B),i,(pA ^ pB))) & dom ((RLine A,i,pA) ^^ (RLine B,i,pB)) = Seg (len ((RLine A,i,pA) ^^ (RLine B,i,pB))) ) by FINSEQ_1:def 3, MATRIX_1:def 3;

now

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (RLine (A ^^ B),i,(pA ^ pB)) . j = ((RLine A,i,pA) ^^ (RLine B,i,pB)) . j )
assume A3: ( 1 <= j & j <= n ) ; :: thesis: (RLine (A ^^ B),i,(pA ^ pB)) . j = ((RLine A,i,pA) ^^ (RLine B,i,pB)) . j
j in NAT by ORDINAL1:def 13;
then A4: j in Seg n by A3;
( pA is Element of (width A) -tuples_on D & pB is Element of (width B) -tuples_on D ) by A1, FINSEQ_2:110;
then pA ^ pB is Element of ((width A) + (width B)) -tuples_on D by FINSEQ_2:127;
then A5: len (pA ^ pB) = (width A) + (width B) by FINSEQ_1:def 18;
A6: width (A ^^ B) = (width A) + (width B) by A3, MATRIX_1:24;

A7: now

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

suppose i = j ; :: thesis: Line (RLine (A ^^ B),i,(pA ^ pB)),j = Line ((RLine A,i,pA) ^^ (RLine B,i,pB)),j

then ( Line (RLine (A ^^ B),i,(pA ^ pB)),j = pA ^ pB & Line (RLine A,i,pA),j = pA & Line (RLine B,i,pB),j = pB ) by A1, A4, A5, A6, MATRIX11:28;
hence Line (RLine (A ^^ B),i,(pA ^ pB)),j = Line ((RLine A,i,pA) ^^ (RLine B,i,pB)),j by A4, Th15; :: thesis: verum

end;

suppose i <> j ; :: thesis: Line (RLine (A ^^ B),i,(pA ^ pB)),j = Line ((RLine A,i,pA) ^^ (RLine B,i,pB)),j

then ( Line (RLine (A ^^ B),i,(pA ^ pB)),j = Line (A ^^ B),j & Line (RLine A,i,pA),j = Line A,j & Line (RLine B,i,pB),j = Line B,j ) by A4, MATRIX11:28;
hence Line (RLine (A ^^ B),i,(pA ^ pB)),j = (Line (RLine A,i,pA),j) ^ (Line (RLine B,i,pB),j) by A4, Th15
.= Line ((RLine A,i,pA) ^^ (RLine B,i,pB)),j by A4, Th15 ;
:: thesis: verum

end;

end;

end;

thus (RLine (A ^^ B),i,(pA ^ pB)) . j = Line (RLine (A ^^ B),i,(pA ^ pB)),j by A4, MATRIX_2:10
.= ((RLine A,i,pA) ^^ (RLine B,i,pB)) . j by A7, A4, MATRIX_2:10 ; :: thesis: verum

end;

hence ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB) by A2, FINSEQ_1:18; :: thesis: verum