let n be Nat; :: thesis: for K being Field
for l being Nat
for a being Element of K
for A being Matrix of n,K st l in dom (1. K,n) holds
(SXLine (1. K,n),l,a) * A = SXLine A,l,a
let K be Field; :: thesis: for l being Nat
for a being Element of K
for A being Matrix of n,K st l in dom (1. K,n) holds
(SXLine (1. K,n),l,a) * A = SXLine A,l,a
let l be Nat; :: thesis: for a being Element of K
for A being Matrix of n,K st l in dom (1. K,n) holds
(SXLine (1. K,n),l,a) * A = SXLine A,l,a
let a be Element of K; :: thesis: for A being Matrix of n,K st l in dom (1. K,n) holds
(SXLine (1. K,n),l,a) * A = SXLine A,l,a
let A be Matrix of n,K; :: thesis: ( l in dom (1. K,n) implies (SXLine (1. K,n),l,a) * A = SXLine A,l,a )
assume A1: l in dom (1. K,n) ; :: thesis: (SXLine (1. K,n),l,a) * A = SXLine A,l,a
set B = SXLine (1. K,n),l,a;
A2: ( len (SXLine (1. K,n),l,a) = len (1. K,n) & len (SXLine (1. K,n),l,a) = n ) by Def2, MATRIX_1:25;
then A3: l in Seg n by A1, FINSEQ_1:def 3;
A4: width (SXLine (1. K,n),l,a) = n by MATRIX_1:25;
A5: width A = n by MATRIX_1:25;
A6: len A = n by MATRIX_1:25;
A7: Indices ((SXLine (1. K,n),l,a) * A) = [:(Seg n),(Seg n):] by MATRIX_1:25;
A8: width (SXLine (1. K,n),l,a) = width (1. K,n) by Th1;
then A9: l in Seg (width (1. K,n)) by A1, A2, A4, FINSEQ_1:def 3;
then A10: [l,l] in Indices (1. K,n) by A1, ZFMISC_1:106;
A11: for i, j being Nat st j in Seg n & i in dom (1. K,n) & i = l holds
((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. K,n) & i = l implies ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j )
assume that
A12: j in Seg n and
A13: i in dom (1. K,n) ; :: thesis: ( not i = l or ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j )
thus ( i = l implies ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j ) :: thesis: verum

proof

reconsider p = Line (1. K,n),l as Element of (width A) -tuples_on the carrier of K by Th1;
reconsider q = Col A,j as Element of (width A) -tuples_on the carrier of K by A6, MATRIX_1:25;
len (Line (1. K,n),l) = width (1. K,n) by MATRIX_1:def 8;
then A14: l in dom (Line (1. K,n),l) by A9, FINSEQ_1:def 3;
( len (Col A,j) = len A & l in Seg n ) by A1, A2, FINSEQ_1:def 3, MATRIX_1:def 9;
then A15: l in dom (Col A,j) by A6, FINSEQ_1:def 3;
A16: ( (Line (1. K,n),l) . l = 1_ K & ( for t being Nat st t in dom (Line (1. K,n),l) & t <> l holds
(Line (1. K,n),l) . t = 0. K ) )

proof

thus (Line (1. K,n),l) . l = 1_ K by A10, MATRIX_3:17; :: thesis: for t being Nat st t in dom (Line (1. K,n),l) & t <> l holds
(Line (1. K,n),l) . t = 0. K
let t be Nat; :: thesis: ( t in dom (Line (1. K,n),l) & t <> l implies (Line (1. K,n),l) . t = 0. K )
assume that
A17: t in dom (Line (1. K,n),l) and
A18: t <> l ; :: thesis: (Line (1. K,n),l) . t = 0. K
t in Seg (len (Line (1. K,n),l)) by A17, FINSEQ_1:def 3;
then t in Seg (width (1. K,n)) by MATRIX_1:def 8;
then [l,t] in Indices (1. K,n) by A1, ZFMISC_1:106;
hence (Line (1. K,n),l) . t = 0. K by A18, MATRIX_3:17; :: thesis: verum

end;

A19: dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg (len A) by A6, MATRIX_1:25
.= dom A by FINSEQ_1:def 3 ;
then (Col A,j) . l = A * l,j by A1, MATRIX_1:def 9;
then consider a1 being Element of K such that
A20: a1 = (Col A,j) . l ;
assume A21: i = l ; :: thesis: ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j
then [i,j] in Indices ((SXLine (1. K,n),l,a) * A) by A3, A7, A12, ZFMISC_1:106;
then ((SXLine (1. K,n),l,a) * A) * i,j = (Line (SXLine (1. K,n),l,a),i) "*" (Col A,j) by A4, A6, MATRIX_3:def 4
.= Sum (mlt (a * p),q) by A1, A21, Th4
.= Sum (a * (mlt p,q)) by FVSUM_1:83
.= a * (Sum (mlt (Line (1. K,n),l),(Col A,j))) by FVSUM_1:92
.= a * a1 by A14, A15, A16, A20, MATRIX_3:19
.= a * (A * l,j) by A1, A19, A20, MATRIX_1:def 9
.= (SXLine A,l,a) * i,j by A5, A12, A13, A21, A19, Def2 ;
hence ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j ; :: thesis: verum

end;

end;

A22: for i, j being Nat st j in Seg n & i in dom (1. K,n) & i <> l holds
((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. K,n) & i <> l implies ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j )
assume that
A23: j in Seg n and
A24: i in dom (1. K,n) ; :: thesis: ( not i <> l or ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j )
A25: i in Seg n by A2, A24, FINSEQ_1:def 3;
then A26: [i,i] in Indices (1. K,n) by A8, A4, A24, ZFMISC_1:106;
thus ( i <> l implies ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j ) :: thesis: verum

proof

A27: ( (Line (1. K,n),i) . i = 1_ K & ( for t being Nat st t in dom (Line (1. K,n),i) & t <> i holds
(Line (1. K,n),i) . t = 0. K ) )

proof

thus (Line (1. K,n),i) . i = 1_ K by A26, MATRIX_3:17; :: thesis: for t being Nat st t in dom (Line (1. K,n),i) & t <> i holds
(Line (1. K,n),i) . t = 0. K
let t be Nat; :: thesis: ( t in dom (Line (1. K,n),i) & t <> i implies (Line (1. K,n),i) . t = 0. K )
assume that
A28: t in dom (Line (1. K,n),i) and
A29: t <> i ; :: thesis: (Line (1. K,n),i) . t = 0. K
t in Seg (len (Line (1. K,n),i)) by A28, FINSEQ_1:def 3;
then t in Seg (width (1. K,n)) by MATRIX_1:def 8;
then [i,t] in Indices (1. K,n) by A24, ZFMISC_1:106;
hence (Line (1. K,n),i) . t = 0. K by A29, MATRIX_3:17; :: thesis: verum

end;

len (Col A,j) = len A by MATRIX_1:def 9;
then A30: i in dom (Col A,j) by A6, A25, FINSEQ_1:def 3;
A31: dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg (len A) by A6, MATRIX_1:25
.= dom A by FINSEQ_1:def 3 ;
len (Line (1. K,n),i) = width (1. K,n) by MATRIX_1:def 8;
then A32: i in dom (Line (1. K,n),i) by A8, A4, A25, FINSEQ_1:def 3;
assume A33: i <> l ; :: thesis: ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j
[i,j] in Indices ((SXLine (1. K,n),l,a) * A) by A7, A23, A25, ZFMISC_1:106;
then ((SXLine (1. K,n),l,a) * A) * i,j = (Line (SXLine (1. K,n),l,a),i) "*" (Col A,j) by A4, A6, MATRIX_3:def 4
.= Sum (mlt (Line (1. K,n),i),(Col A,j)) by A1, A24, A33, Th4
.= (Col A,j) . i by A32, A30, A27, MATRIX_3:19
.= A * i,j by A24, A31, MATRIX_1:def 9
.= (SXLine A,l,a) * i,j by A5, A23, A24, A33, A31, Def2 ;
hence ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j ; :: thesis: verum

end;

end;

A34: for i, j being Nat st [i,j] in Indices ((SXLine (1. K,n),l,a) * A) holds
((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((SXLine (1. K,n),l,a) * A) implies ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j )
assume [i,j] in Indices ((SXLine (1. K,n),l,a) * A) ; :: thesis: ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j
then A35: ( i in Seg n & j in Seg n ) by A7, ZFMISC_1:106;
dom (1. K,n) = Seg (len (1. K,n)) by FINSEQ_1:def 3
.= Seg n by MATRIX_1:25 ;
hence ((SXLine (1. K,n),l,a) * A) * i,j = (SXLine A,l,a) * i,j by A11, A22, A35; :: thesis: verum

end;

A36: ( len ((SXLine (1. K,n),l,a) * A) = n & width ((SXLine (1. K,n),l,a) * A) = n ) by MATRIX_1:25;
( len (SXLine A,l,a) = len A & width (SXLine A,l,a) = width A ) by Def2, Th1;
hence (SXLine (1. K,n),l,a) * A = SXLine A,l,a by A6, A5, A36, A34, MATRIX_1:21; :: thesis: verum