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 () -tuples_on D & pB is Element of () -tuples_on D ) by ;
then pA ^ pB is Tuple of () + (),D ;
then pA ^ pB is Element of (() + ()) -tuples_on D by FINSEQ_2:131;
then A4: len (pA ^ pB) = () + () 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) = () + () by ;
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 ;
( Line ((RLine ((A ^^ B),i,(pA ^ pB))),j) = pA ^ pB & Line ((RLine (A,i,pA)),j) = pA ) by ;
hence Line ((RLine ((A ^^ B),i,(pA ^ pB))),j) = Line (((RLine (A,i,pA)) ^^ (RLine (B,i,pB))),j) by ; :: 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 ;
( Line ((RLine ((A ^^ B),i,(pA ^ pB))),j) = Line ((A ^^ B),j) & Line ((RLine (A,i,pA)),j) = Line (A,j) ) by ;
hence Line ((RLine ((A ^^ B),i,(pA ^ pB))),j) = (Line ((RLine (A,i,pA)),j)) ^ (Line ((RLine (B,i,pB)),j)) by
.= Line (((RLine (A,i,pA)) ^^ (RLine (B,i,pB))),j) by ;
:: thesis: verum
end;
end;
end;
thus (RLine ((A ^^ B),i,(pA ^ pB))) . j = Line ((RLine ((A ^^ B),i,(pA ^ pB))),j) by
.= ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) . j by ; :: 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