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 that
A1: len pA = width A and
A2: len pB = width B ; :: thesis: ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)
set RB = RLine B,i,pB;
set RA = RLine A,i,pA;
set AB = A ^^ B;
set RAB = RLine (A ^^ B),i,(pA ^ pB);
set Rab = (RLine A,i,pA) ^^ (RLine B,i,pB);

A3: now

( pA is Element of (width A) -tuples_on D & pB is Element of (width B) -tuples_on D ) by A1, A2, FINSEQ_2:110;
then pA ^ pB is Tuple of (width A) + (width B),D by FINSEQ_2:127;
then pA ^ pB is Element of ((width A) + (width B)) -tuples_on D by FINSEQ_2:151;
then A4: len (pA ^ pB) = (width A) + (width B) by FINSEQ_1:def 18;
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 A5: ( 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 A6: j in Seg n by A5;
A7: width (A ^^ B) = (width A) + (width B) by A5, MATRIX_1:24;

A8: now

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

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

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

end;

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

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

end;

end;

end;

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

end;

( len (RLine (A ^^ B),i,(pA ^ pB)) = n & len ((RLine A,i,pA) ^^ (RLine B,i,pB)) = n ) by MATRIX_1:def 3;
hence ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB) by A3, FINSEQ_1:18; :: thesis: verum