let i, 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) holds

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

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

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

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

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

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

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

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

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

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

set LA = Line (A9,i);

set LB = Line (B9,i);

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

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

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

A2: ( len (a * (Line (B9,i))) = len (Line (B9,i)) & len (Line (B9,i)) = width B9 ) by CARD_1:def 7, MATRIXR1:16;

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

A4: ( len (a * (Line (A9,i))) = len (Line (A9,i)) & len (Line (A9,i)) = width A9 ) by CARD_1:def 7, MATRIXR1:16;

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

assume A6: X in Solutions_of (A9,B9) ; :: thesis: X in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))

then consider X1 being Matrix of K such that

A7: X = X1 and

A8: len X1 = width A9 and

A9: width X1 = width B9 and

A10: A9 * X1 = B9 ;

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

A11: width (RLine (A9,i,(a * (Line (A9,i))))) = width A9 by A4, MATRIX11:def 3;

then A12: ( len ((RLine (A9,i,(a * (Line (A9,i))))) * X1) = len (RLine (A9,i,(a * (Line (A9,i))))) & width ((RLine (A9,i,(a * (Line (A9,i))))) * X1) = width X1 ) by A8, MATRIX_3:def 4;

A13: len A9 = len B9 by A6, Th33;

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

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

then (RLine (A9,i,(a * (Line (A9,i))))) * X1 = RLine (B9,i,(a * (Line (B9,i)))) by A9, A13, A5, A3, A12, A15, MATRIX_0:21;

hence X in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) by A7, A8, A9, A11, A3; :: 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) holds

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

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

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

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

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

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

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

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

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

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

set LA = Line (A9,i);

set LB = Line (B9,i);

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

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

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

A2: ( len (a * (Line (B9,i))) = len (Line (B9,i)) & len (Line (B9,i)) = width B9 ) by CARD_1:def 7, MATRIXR1:16;

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

A4: ( len (a * (Line (A9,i))) = len (Line (A9,i)) & len (Line (A9,i)) = width A9 ) by CARD_1:def 7, MATRIXR1:16;

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

assume A6: X in Solutions_of (A9,B9) ; :: thesis: X in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))

then consider X1 being Matrix of K such that

A7: X = X1 and

A8: len X1 = width A9 and

A9: width X1 = width B9 and

A10: A9 * X1 = B9 ;

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

A11: width (RLine (A9,i,(a * (Line (A9,i))))) = width A9 by A4, MATRIX11:def 3;

then A12: ( len ((RLine (A9,i,(a * (Line (A9,i))))) * X1) = len (RLine (A9,i,(a * (Line (A9,i))))) & width ((RLine (A9,i,(a * (Line (A9,i))))) * X1) = width X1 ) by A8, MATRIX_3:def 4;

A13: len A9 = len B9 by A6, Th33;

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

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

A15: now :: thesis: for j, k being Nat st [j,k] in Indices (RLine (B9,i,(a * (Line (B9,i))))) holds

(RLine (B9,i,(a * (Line (B9,i))))) * (j,k) = ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k)

len (RLine (B9,i,(a * (Line (B9,i))))) = len B9
by A2, MATRIX11:def 3;(RLine (B9,i,(a * (Line (B9,i))))) * (j,k) = ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k)

len B9 = m
by MATRIX_0:def 2;

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

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

assume A17: [j,k] in Indices (RLine (B9,i,(a * (Line (B9,i))))) ; :: thesis: (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) = ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k)

A18: j in dom B9 by A1, A17, ZFMISC_1:87;

A19: k in Seg (width B9) by A1, A17, ZFMISC_1:87;

then B9 * (i,k) = (Line (B9,i)) . k by MATRIX_0:def 7;

then reconsider LBk = (Line (B9,i)) . k as Element of K ;

A20: B9 * (j,k) = (Line (A9,j)) "*" (Col (X1,k)) by A8, A10, A1, A17, MATRIX_3:def 4;

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

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

assume A17: [j,k] in Indices (RLine (B9,i,(a * (Line (B9,i))))) ; :: thesis: (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) = ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k)

A18: j in dom B9 by A1, A17, ZFMISC_1:87;

A19: k in Seg (width B9) by A1, A17, ZFMISC_1:87;

then B9 * (i,k) = (Line (B9,i)) . k by MATRIX_0:def 7;

then reconsider LBk = (Line (B9,i)) . k as Element of K ;

A20: B9 * (j,k) = (Line (A9,j)) "*" (Col (X1,k)) by A8, A10, A1, A17, MATRIX_3:def 4;

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

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

end;

suppose A21:
j = i
; :: thesis: ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (RLine (B9,i,(a * (Line (B9,i))))) * (j,k)

then
Line ((RLine (A9,i,(a * (Line (A9,i))))),i) = a * (Line (A9,i))
by A4, A18, A16, MATRIX11:28;

hence ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (a * (Line (A9,i))) "*" (Col (X1,k)) by A8, A11, A14, A1, A17, A21, MATRIX_3:def 4

.= Sum (a * (mlt ((Line (A9,i)),(Col (X1,k))))) by A8, FVSUM_1:68

.= a * (Sum (mlt ((Line (A9,i)),(Col (X1,k))))) by FVSUM_1:73

.= a * LBk by A19, A20, A21, MATRIX_0:def 7

.= (a * (Line (B9,i))) . k by A19, FVSUM_1:51

.= (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) by A2, A1, A17, A21, MATRIX11:def 3 ;

:: thesis: verum

end;hence ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (a * (Line (A9,i))) "*" (Col (X1,k)) by A8, A11, A14, A1, A17, A21, MATRIX_3:def 4

.= Sum (a * (mlt ((Line (A9,i)),(Col (X1,k))))) by A8, FVSUM_1:68

.= a * (Sum (mlt ((Line (A9,i)),(Col (X1,k))))) by FVSUM_1:73

.= a * LBk by A19, A20, A21, MATRIX_0:def 7

.= (a * (Line (B9,i))) . k by A19, FVSUM_1:51

.= (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) by A2, A1, A17, A21, MATRIX11:def 3 ;

:: thesis: verum

suppose A22:
j <> i
; :: thesis: ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (RLine (B9,i,(a * (Line (B9,i))))) * (j,k)

then
Line ((RLine (A9,i,(a * (Line (A9,i))))),j) = Line (A9,j)
by A18, A16, MATRIX11:28;

hence ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (Line (A9,j)) "*" (Col (X1,k)) by A8, A11, A14, A1, A17, MATRIX_3:def 4

.= B9 * (j,k) by A8, A10, A1, A17, MATRIX_3:def 4

.= (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) by A2, A1, A17, A22, MATRIX11:def 3 ;

:: thesis: verum

end;hence ((RLine (A9,i,(a * (Line (A9,i))))) * X1) * (j,k) = (Line (A9,j)) "*" (Col (X1,k)) by A8, A11, A14, A1, A17, MATRIX_3:def 4

.= B9 * (j,k) by A8, A10, A1, A17, MATRIX_3:def 4

.= (RLine (B9,i,(a * (Line (B9,i))))) * (j,k) by A2, A1, A17, A22, MATRIX11:def 3 ;

:: thesis: verum

then (RLine (A9,i,(a * (Line (A9,i))))) * X1 = RLine (B9,i,(a * (Line (B9,i)))) by A9, A13, A5, A3, A12, A15, MATRIX_0:21;

hence X in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i)))))) by A7, A8, A9, A11, A3; :: thesis: verum