let i, k, m, n 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 :: thesis: for j being Nat st 1 <= j & j <= n holds
(RLine ((A ^^ B),i,(pA ^ pB))) . j = ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) . j

( pA is Element of (width A) -tuples_on D & pB is Element of (width B) -tuples_on D ) by A1, A2, FINSEQ_2:92;
then pA ^ pB is Tuple of (width A) + (width B),D ;
then pA ^ pB is Element of ((width A) + (width B)) -tuples_on D by FINSEQ_2:131;
then A4: len (pA ^ pB) = (width A) + (width B) by CARD_1:def 7;
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
A6: j in Seg n by A5;
A7: width (A ^^ B) = (width A) + (width B) by A5, MATRIX_0:23;

A8: now :: thesis: Line ((RLine ((A ^^ B),i,(pA ^ pB))),j) = Line (((RLine (A,i,pA)) ^^ (RLine (B,i,pB))),j)

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_0:52
.= ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) . j by A6, A8, MATRIX_0:52 ; :: thesis: verum

end;

( len (RLine ((A ^^ B),i,(pA ^ pB))) = n & len ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) = n ) by MATRIX_0:def 2;
hence ReplaceLine ((A ^^ B),i,(pA ^ pB)) = (ReplaceLine (A,i,pA)) ^^ (ReplaceLine (B,i,pB)) by A3; :: thesis: verum