let n, m, k, i be Nat; :: thesis: for K being Field
for a being Element of
for X being Matrix of
for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let K be Field; :: thesis: for a being Element of
for X being Matrix of
for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let a be Element of ; :: thesis: for X being Matrix of
for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let X be Matrix of ; :: thesis: for A' being Matrix of the carrier of K,m,
for B' being Matrix of the carrier of K,m, st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let A' be Matrix of the carrier of K,m,; :: thesis: for B' being Matrix of the carrier of K,m, st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
let B' be Matrix of the carrier of K,m,; :: thesis: ( X in Solutions_of A',B' implies X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) )
set LA = Line A',i;
set LB = Line B',i;
set RA = RLine A',i,(a * (Line A',i));
set RB = RLine B',i,(a * (Line B',i));
A1: Indices (RLine B',i,(a * (Line B',i))) = Indices B' by MATRIX_1:27;
A2: ( len (a * (Line B',i)) = len (Line B',i) & len (Line B',i) = width B' ) by FINSEQ_1:def 18, MATRIXR1:16;
then A3: width (RLine B',i,(a * (Line B',i))) = width B' by MATRIX11:def 3;
A4: ( len (a * (Line A',i)) = len (Line A',i) & len (Line A',i) = width A' ) by FINSEQ_1:def 18, MATRIXR1:16;
then A5: len (RLine A',i,(a * (Line A',i))) = len A' by MATRIX11:def 3;
assume A6: X in Solutions_of A',B' ; :: thesis: X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))
then consider X1 being Matrix of such that
A7: X = X1 and
A8: len X1 = width A' and
A9: width X1 = width B' and
A10: A' * X1 = B' ;
set RX = (RLine A',i,(a * (Line A',i))) * X1;
A11: width (RLine A',i,(a * (Line A',i))) = width A' by A4, MATRIX11:def 3;
then A12: ( len ((RLine A',i,(a * (Line A',i))) * X1) = len (RLine A',i,(a * (Line A',i))) & width ((RLine A',i,(a * (Line A',i))) * X1) = width X1 ) by A8, MATRIX_3:def 4;
A13: len A' = len B' by A6, Th33;
then dom B' = Seg (len (RLine A',i,(a * (Line A',i)))) by A5, FINSEQ_1:def 3;
then A14: Indices ((RLine A',i,(a * (Line A',i))) * X1) = Indices B' by A9, A12, FINSEQ_1:def 3;

A15: now

len B' = m by MATRIX_1:def 3;
then A16: dom B' = Seg m by FINSEQ_1:def 3;
let j, k be Nat; :: thesis: ( [j,k] in Indices (RLine B',i,(a * (Line B',i))) implies (RLine B',i,(a * (Line B',i))) * j,k = ((RLine A',i,(a * (Line A',i))) * X1) * j,k )
assume A17: [j,k] in Indices (RLine B',i,(a * (Line B',i))) ; :: thesis: (RLine B',i,(a * (Line B',i))) * j,k = ((RLine A',i,(a * (Line A',i))) * X1) * j,k
A18: j in dom B' by A1, A17, ZFMISC_1:106;
A19: k in Seg (width B') by A1, A17, ZFMISC_1:106;
then B' * i,k = (Line B',i) . k by MATRIX_1:def 8;
then reconsider LBk = (Line B',i) . k as Element of ;
A20: B' * j,k = (Line A',j) "*" (Col X1,k) by A8, A10, A1, A17, MATRIX_3:def 4;

now

per cases ( j = i or j <> i ) ;

suppose A21: j = i ; :: thesis: ((RLine A',i,(a * (Line A',i))) * X1) * j,k = (RLine B',i,(a * (Line B',i))) * j,k

then Line (RLine A',i,(a * (Line A',i))),i = a * (Line A',i) by A4, A18, A16, MATRIX11:28;
hence ((RLine A',i,(a * (Line A',i))) * X1) * j,k = (a * (Line A',i)) "*" (Col X1,k) by A8, A11, A14, A1, A17, A21, MATRIX_3:def 4
.= Sum (a * (mlt (Line A',i),(Col X1,k))) by A8, FVSUM_1:82
.= a * (Sum (mlt (Line A',i),(Col X1,k))) by FVSUM_1:92
.= a * LBk by A19, A20, A21, MATRIX_1:def 8
.= (a * (Line B',i)) . k by A19, FVSUM_1:63
.= (RLine B',i,(a * (Line B',i))) * j,k by A2, A1, A17, A21, MATRIX11:def 3 ;
:: thesis: verum

end;

suppose A22: j <> i ; :: thesis: ((RLine A',i,(a * (Line A',i))) * X1) * j,k = (RLine B',i,(a * (Line B',i))) * j,k

then Line (RLine A',i,(a * (Line A',i))),j = Line A',j by A18, A16, MATRIX11:28;
hence ((RLine A',i,(a * (Line A',i))) * X1) * j,k = (Line A',j) "*" (Col X1,k) by A8, A11, A14, A1, A17, MATRIX_3:def 4
.= B' * j,k by A8, A10, A1, A17, MATRIX_3:def 4
.= (RLine B',i,(a * (Line B',i))) * j,k by A2, A1, A17, A22, MATRIX11:def 3 ;
:: thesis: verum

end;

end;

end;

hence (RLine B',i,(a * (Line B',i))) * j,k = ((RLine A',i,(a * (Line A',i))) * X1) * j,k ; :: thesis: verum

end;

len (RLine B',i,(a * (Line B',i))) = len B' by A2, MATRIX11:def 3;
then (RLine A',i,(a * (Line A',i))) * X1 = RLine B',i,(a * (Line B',i)) by A9, A13, A5, A3, A12, A15, MATRIX_1:21;
hence X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i))) by A7, A8, A9, A11, A3; :: thesis: verum