let i, j, k, m, n be Nat; :: thesis: for K being Field

for a being Element of K

for X being Matrix of K

for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let K be Field; :: thesis: for a being Element of K

for X being Matrix of K

for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let a be Element of K; :: thesis: for X being Matrix of K

for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let X be Matrix of K; :: thesis: for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let B9 be Matrix of m,k,K; :: thesis: ( X in Solutions_of (A9,B9) & j in Seg m implies X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) )

assume that

A1: X in Solutions_of (A9,B9) and

A2: j in Seg m ; :: thesis: X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

consider X1 being Matrix of K such that

A3: X = X1 and

A4: len X1 = width A9 and

A5: width X1 = width B9 and

A6: A9 * X1 = B9 by A1;

set LAj = Line (A9,j);

set LAi = Line (A9,i);

set RA = RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))));

A7: len ((Line (A9,i)) + (a * (Line (A9,j)))) = width A9 by CARD_1:def 7;

then A8: len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = len A9 by MATRIX11:def 3;

set RX = (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1;

A9: width (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = width A9 by A7, MATRIX11:def 3;

then A10: ( len ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) & width ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = width X1 ) by A4, MATRIX_3:def 4;

A11: len A9 = len B9 by A1, Th33;

then dom B9 = Seg (len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))) by A8, FINSEQ_1:def 3;

then A12: Indices ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = Indices B9 by A5, A10, FINSEQ_1:def 3;

set LBj = Line (B9,j);

set LBi = Line (B9,i);

set RB = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))));

A13: Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = Indices B9 by MATRIX_0:26;

A14: len ((Line (B9,i)) + (a * (Line (B9,j)))) = width B9 by CARD_1:def 7;

then A15: width (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = width B9 by MATRIX11:def 3;

A16: ( len (a * (Line (A9,j))) = width A9 & len (Line (A9,i)) = width A9 ) by CARD_1:def 7;

then (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1 = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))) by A5, A11, A8, A15, A10, A17, MATRIX_0:21;

hence X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) by A3, A4, A5, A9, A15; :: thesis: verum

for a being Element of K

for X being Matrix of K

for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let K be Field; :: thesis: for a being Element of K

for X being Matrix of K

for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let a be Element of K; :: thesis: for X being Matrix of K

for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let X be Matrix of K; :: thesis: for A9 being Matrix of m,n,K

for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds

X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let B9 be Matrix of m,k,K; :: thesis: ( X in Solutions_of (A9,B9) & j in Seg m implies X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) )

assume that

A1: X in Solutions_of (A9,B9) and

A2: j in Seg m ; :: thesis: X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

consider X1 being Matrix of K such that

A3: X = X1 and

A4: len X1 = width A9 and

A5: width X1 = width B9 and

A6: A9 * X1 = B9 by A1;

set LAj = Line (A9,j);

set LAi = Line (A9,i);

set RA = RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))));

A7: len ((Line (A9,i)) + (a * (Line (A9,j)))) = width A9 by CARD_1:def 7;

then A8: len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = len A9 by MATRIX11:def 3;

set RX = (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1;

A9: width (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = width A9 by A7, MATRIX11:def 3;

then A10: ( len ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) & width ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = width X1 ) by A4, MATRIX_3:def 4;

A11: len A9 = len B9 by A1, Th33;

then dom B9 = Seg (len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))) by A8, FINSEQ_1:def 3;

then A12: Indices ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = Indices B9 by A5, A10, FINSEQ_1:def 3;

set LBj = Line (B9,j);

set LBi = Line (B9,i);

set RB = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))));

A13: Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = Indices B9 by MATRIX_0:26;

A14: len ((Line (B9,i)) + (a * (Line (B9,j)))) = width B9 by CARD_1:def 7;

then A15: width (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = width B9 by MATRIX11:def 3;

A16: ( len (a * (Line (A9,j))) = width A9 & len (Line (A9,i)) = width A9 ) by CARD_1:def 7;

A17: now :: thesis: for o, p being Nat st [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) holds

(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)

len (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = len B9
by A14, MATRIX11:def 3;(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)

A18:
rng (a * (Line (B9,j))) c= the carrier of K
by FINSEQ_1:def 4;

let o, p be Nat; :: thesis: ( [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) implies (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) )

assume A19: [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) ; :: thesis: (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)

A20: o in dom B9 by A13, A19, ZFMISC_1:87;

A21: B9 * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by A4, A6, A13, A19, MATRIX_3:def 4;

reconsider CX = Col (X1,p) as Element of (width A9) -tuples_on the carrier of K by A4;

A22: len (Col (X1,p)) = width A9 by A4, MATRIX_0:def 8;

A23: p in Seg (width B9) by A13, A19, ZFMISC_1:87;

then ( B9 * (o,p) = (Line (B9,o)) . p & B9 * (j,p) = (Line (B9,j)) . p ) by MATRIX_0:def 7;

then reconsider LBop = (Line (B9,o)) . p, LBjp = (Line (B9,j)) . p as Element of the carrier of K ;

p in dom (a * (Line (B9,j))) by A23, FINSEQ_2:124;

then (a * (Line (B9,j))) . p in rng (a * (Line (B9,j))) by FUNCT_1:def 3;

then reconsider aLBjp = (a * (Line (B9,j))) . p as Element of K by A18;

len B9 = m by MATRIX_0:def 2;

then A24: dom B9 = Seg m by FINSEQ_1:def 3;

then [j,p] in Indices B9 by A2, A23, ZFMISC_1:87;

then A25: B9 * (j,p) = (Line (A9,j)) "*" (Col (X1,p)) by A4, A6, MATRIX_3:def 4;

end;let o, p be Nat; :: thesis: ( [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) implies (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) )

assume A19: [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) ; :: thesis: (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)

A20: o in dom B9 by A13, A19, ZFMISC_1:87;

A21: B9 * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by A4, A6, A13, A19, MATRIX_3:def 4;

reconsider CX = Col (X1,p) as Element of (width A9) -tuples_on the carrier of K by A4;

A22: len (Col (X1,p)) = width A9 by A4, MATRIX_0:def 8;

A23: p in Seg (width B9) by A13, A19, ZFMISC_1:87;

then ( B9 * (o,p) = (Line (B9,o)) . p & B9 * (j,p) = (Line (B9,j)) . p ) by MATRIX_0:def 7;

then reconsider LBop = (Line (B9,o)) . p, LBjp = (Line (B9,j)) . p as Element of the carrier of K ;

p in dom (a * (Line (B9,j))) by A23, FINSEQ_2:124;

then (a * (Line (B9,j))) . p in rng (a * (Line (B9,j))) by FUNCT_1:def 3;

then reconsider aLBjp = (a * (Line (B9,j))) . p as Element of K by A18;

len B9 = m by MATRIX_0:def 2;

then A24: dom B9 = Seg m by FINSEQ_1:def 3;

then [j,p] in Indices B9 by A2, A23, ZFMISC_1:87;

then A25: B9 * (j,p) = (Line (A9,j)) "*" (Col (X1,p)) by A4, A6, MATRIX_3:def 4;

now :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)end;

hence
(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)
; :: thesis: verumper cases
( o = i or o <> i )
;

end;

suppose A26:
o = i
; :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)

then
Line ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),o) = (Line (A9,i)) + (a * (Line (A9,j)))
by A7, A20, A24, MATRIX11:28;

hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = ((Line (A9,i)) + (a * (Line (A9,j)))) "*" CX by A4, A9, A12, A13, A19, MATRIX_3:def 4

.= Sum ((mlt ((Line (A9,i)),CX)) + (mlt ((a * (Line (A9,j))),CX))) by A16, A22, MATRIX_4:56

.= Sum ((mlt ((Line (A9,i)),CX)) + (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:68

.= (Sum (mlt ((Line (A9,i)),CX))) + (Sum (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:76

.= (B9 * (o,p)) + (a * (B9 * (j,p))) by A21, A25, A26, FVSUM_1:73

.= LBop + (a * (B9 * (j,p))) by A23, MATRIX_0:def 7

.= LBop + (a * LBjp) by A23, MATRIX_0:def 7

.= LBop + aLBjp by A23, FVSUM_1:51

.= ((Line (B9,i)) + (a * (Line (B9,j)))) . p by A23, A26, FVSUM_1:18

.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by A14, A13, A19, A26, MATRIX11:def 3 ;

:: thesis: verum

end;hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = ((Line (A9,i)) + (a * (Line (A9,j)))) "*" CX by A4, A9, A12, A13, A19, MATRIX_3:def 4

.= Sum ((mlt ((Line (A9,i)),CX)) + (mlt ((a * (Line (A9,j))),CX))) by A16, A22, MATRIX_4:56

.= Sum ((mlt ((Line (A9,i)),CX)) + (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:68

.= (Sum (mlt ((Line (A9,i)),CX))) + (Sum (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:76

.= (B9 * (o,p)) + (a * (B9 * (j,p))) by A21, A25, A26, FVSUM_1:73

.= LBop + (a * (B9 * (j,p))) by A23, MATRIX_0:def 7

.= LBop + (a * LBjp) by A23, MATRIX_0:def 7

.= LBop + aLBjp by A23, FVSUM_1:51

.= ((Line (B9,i)) + (a * (Line (B9,j)))) . p by A23, A26, FVSUM_1:18

.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by A14, A13, A19, A26, MATRIX11:def 3 ;

:: thesis: verum

suppose A27:
o <> i
; :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)

then
Line ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),o) = Line (A9,o)
by A20, A24, MATRIX11:28;

hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by A4, A9, A12, A13, A19, MATRIX_3:def 4

.= B9 * (o,p) by A4, A6, A13, A19, MATRIX_3:def 4

.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by A14, A13, A19, A27, MATRIX11:def 3 ;

:: thesis: verum

end;hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by A4, A9, A12, A13, A19, MATRIX_3:def 4

.= B9 * (o,p) by A4, A6, A13, A19, MATRIX_3:def 4

.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by A14, A13, A19, A27, MATRIX11:def 3 ;

:: thesis: verum

then (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1 = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))) by A5, A11, A8, A15, A10, A17, MATRIX_0:21;

hence X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) by A3, A4, A5, A9, A15; :: thesis: verum