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));

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

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

( len (RLine ((A ^^ B),i,(pA ^ pB))) = n & len ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) = n )
by MATRIX_0:def 2;(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;

.= ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) . j by A6, A8, MATRIX_0:52 ; :: thesis: verum

end;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)end;

thus (RLine ((A ^^ B),i,(pA ^ pB))) . j =
Line ((RLine ((A ^^ B),i,(pA ^ pB))),j)
by A6, MATRIX_0:52
per cases
( i = j or i <> j )
;

end;

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;( 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

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;( 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

.= ((RLine (A,i,pA)) ^^ (RLine (B,i,pB))) . j by A6, A8, MATRIX_0:52 ; :: thesis: verum

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