let k, l, n be Nat; :: thesis: for K being comRing
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds
(ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k)
let K be comRing; :: thesis: for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds
(ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k)
let A be Matrix of n,K; :: thesis: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) implies (ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k) )
assume that
A1: l in dom (1. (K,n)) and
A2: k in dom (1. (K,n)) ; :: thesis: (ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k)
set B = ILine ((1. (K,n)),l,k);
A3: ( len (ILine ((1. (K,n)),l,k)) = len (1. (K,n)) & len (ILine ((1. (K,n)),l,k)) = n ) by Def1, MATRIX_0:24;
then A4: l in Seg n by A1, FINSEQ_1:def 3;
A5: k in Seg n by A2, A3, FINSEQ_1:def 3;
A6: width (ILine ((1. (K,n)),l,k)) = n by MATRIX_0:24;
A7: Indices ((ILine ((1. (K,n)),l,k)) * A) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A8: width A = n by MATRIX_0:24;
A9: len A = n by MATRIX_0:24;
A10: width (ILine ((1. (K,n)),l,k)) = width (1. (K,n)) by Th1;
A11: for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i <> l & i <> k holds
((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. (K,n)) & i <> l & i <> k implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
assume that
A12: j in Seg n and
A13: i in dom (1. (K,n)) ; :: thesis: ( not i <> l or not i <> k or ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
A14: i in Seg n by A3, A13, FINSEQ_1:def 3;
then A15: [i,i] in Indices (1. (K,n)) by A10, A6, A13, ZFMISC_1:87;
thus ( i <> l & i <> k implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ) :: thesis: verum

proof

A16: ( (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 A15, MATRIX_3:15; :: 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
A17: t in dom (Line ((1. (K,n)),i)) and
A18: t <> i ; :: thesis: (Line ((1. (K,n)),i)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),i))) by A17, FINSEQ_1:def 3;
then t in Seg (width (1. (K,n))) by MATRIX_0:def 7;
then [i,t] in Indices (1. (K,n)) by A13, ZFMISC_1:87;
hence (Line ((1. (K,n)),i)) . t = 0. K by A18, MATRIX_3:15; :: thesis: verum

end;

len (Col (A,j)) = len A by MATRIX_0:def 8;
then A19: i in dom (Col (A,j)) by A9, A14, FINSEQ_1:def 3;
A20: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def 3
.= Seg (len A) by A9, MATRIX_0:24
.= dom A by FINSEQ_1:def 3 ;
len (Line ((1. (K,n)),i)) = width (1. (K,n)) by MATRIX_0:def 7;
then A21: i in dom (Line ((1. (K,n)),i)) by A10, A6, A14, FINSEQ_1:def 3;
assume A22: ( i <> l & i <> k ) ; :: thesis: ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)
[i,j] in Indices ((ILine ((1. (K,n)),l,k)) * A) by A7, A12, A14, ZFMISC_1:87;
then ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (Line ((ILine ((1. (K,n)),l,k)),i)) "*" (Col (A,j)) by A6, A9, MATRIX_3:def 4
.= Sum (mlt ((Line ((1. (K,n)),i)),(Col (A,j)))) by A1, A2, A13, A22, Th2
.= (Col (A,j)) . i by A21, A19, A16, MATRIX_3:17
.= A * (i,j) by A13, A20, MATRIX_0:def 8
.= (ILine (A,l,k)) * (i,j) by A8, A12, A13, A22, A20, Def1 ;
hence ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ; :: thesis: verum

end;

end;

A23: l in Seg (width (1. (K,n))) by A1, A10, A3, A6, FINSEQ_1:def 3;
then A24: [l,l] in Indices (1. (K,n)) by A1, ZFMISC_1:87;
A25: for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i = k holds
((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. (K,n)) & i = k implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
assume that
A26: j in Seg n and
A27: i in dom (1. (K,n)) ; :: thesis: ( not i = k or ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
thus ( i = k implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ) :: thesis: verum

proof

A28: ( (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 A24, MATRIX_3:15; :: 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
A29: t in dom (Line ((1. (K,n)),l)) and
A30: t <> l ; :: thesis: (Line ((1. (K,n)),l)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),l))) by A29, FINSEQ_1:def 3;
then t in Seg (width (1. (K,n))) by MATRIX_0:def 7;
then [l,t] in Indices (1. (K,n)) by A1, ZFMISC_1:87;
hence (Line ((1. (K,n)),l)) . t = 0. K by A30, MATRIX_3:15; :: thesis: verum

end;

len (Line ((1. (K,n)),l)) = width (1. (K,n)) by MATRIX_0:def 7;
then A31: l in dom (Line ((1. (K,n)),l)) by A23, FINSEQ_1:def 3;
( len (Col (A,j)) = len A & l in Seg n ) by A1, A3, FINSEQ_1:def 3, MATRIX_0:def 8;
then A32: l in dom (Col (A,j)) by A9, FINSEQ_1:def 3;
A33: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def 3
.= Seg (len A) by A9, MATRIX_0:24
.= dom A by FINSEQ_1:def 3 ;
assume A34: i = k ; :: thesis: ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)
then [i,j] in Indices ((ILine ((1. (K,n)),l,k)) * A) by A5, A7, A26, ZFMISC_1:87;
then ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (Line ((ILine ((1. (K,n)),l,k)),i)) "*" (Col (A,j)) by A6, A9, MATRIX_3:def 4
.= Sum (mlt ((Line ((1. (K,n)),l)),(Col (A,j)))) by A1, A2, A34, Th2
.= (Col (A,j)) . l by A31, A32, A28, MATRIX_3:17
.= A * (l,j) by A1, A33, MATRIX_0:def 8
.= (ILine (A,l,k)) * (i,j) by A8, A26, A27, A34, A33, Def1 ;
hence ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ; :: thesis: verum

end;

end;

A35: k in Seg (width (1. (K,n))) by A2, A10, A3, A6, FINSEQ_1:def 3;
then A36: [k,k] in Indices (1. (K,n)) by A2, ZFMISC_1:87;
A37: for i, j being Nat st j in Seg n & i in dom (1. (K,n)) & i = l holds
((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)

proof

let i, j be Nat; :: thesis: ( j in Seg n & i in dom (1. (K,n)) & i = l implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
assume that
A38: j in Seg n and
A39: i in dom (1. (K,n)) ; :: thesis: ( not i = l or ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
thus ( i = l implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ) :: thesis: verum

proof

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

proof

thus (Line ((1. (K,n)),k)) . k = 1_ K by A36, MATRIX_3:15; :: thesis: for t being Nat st t in dom (Line ((1. (K,n)),k)) & t <> k holds
(Line ((1. (K,n)),k)) . t = 0. K
let t be Nat; :: thesis: ( t in dom (Line ((1. (K,n)),k)) & t <> k implies (Line ((1. (K,n)),k)) . t = 0. K )
assume that
A41: t in dom (Line ((1. (K,n)),k)) and
A42: t <> k ; :: thesis: (Line ((1. (K,n)),k)) . t = 0. K
t in Seg (len (Line ((1. (K,n)),k))) by A41, FINSEQ_1:def 3;
then t in Seg (width (1. (K,n))) by MATRIX_0:def 7;
then [k,t] in Indices (1. (K,n)) by A2, ZFMISC_1:87;
hence (Line ((1. (K,n)),k)) . t = 0. K by A42, MATRIX_3:15; :: thesis: verum

end;

len (Line ((1. (K,n)),k)) = width (1. (K,n)) by MATRIX_0:def 7;
then A43: k in dom (Line ((1. (K,n)),k)) by A35, FINSEQ_1:def 3;
( len (Col (A,j)) = len A & k in Seg n ) by A2, A3, FINSEQ_1:def 3, MATRIX_0:def 8;
then A44: k in dom (Col (A,j)) by A9, FINSEQ_1:def 3;
A45: dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def 3
.= Seg (len A) by A9, MATRIX_0:24
.= dom A by FINSEQ_1:def 3 ;
assume A46: i = l ; :: thesis: ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)
then [i,j] in Indices ((ILine ((1. (K,n)),l,k)) * A) by A4, A7, A38, ZFMISC_1:87;
then ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (Line ((ILine ((1. (K,n)),l,k)),i)) "*" (Col (A,j)) by A6, A9, MATRIX_3:def 4
.= Sum (mlt ((Line ((1. (K,n)),k)),(Col (A,j)))) by A1, A2, A46, Th2
.= (Col (A,j)) . k by A43, A44, A40, MATRIX_3:17
.= A * (k,j) by A2, A45, MATRIX_0:def 8
.= (ILine (A,l,k)) * (i,j) by A8, A38, A39, A46, A45, Def1 ;
hence ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ; :: thesis: verum

end;

end;

A47: for i, j being Nat st [i,j] in Indices ((ILine ((1. (K,n)),l,k)) * A) holds
((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((ILine ((1. (K,n)),l,k)) * A) implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) )
assume A48: [i,j] in Indices ((ILine ((1. (K,n)),l,k)) * A) ; :: thesis: ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j)
dom (1. (K,n)) = Seg (len (1. (K,n))) by FINSEQ_1:def 3
.= Seg n by MATRIX_0:24 ;
then A49: i in dom (1. (K,n)) by A7, A48, ZFMISC_1:87;
A50: j in Seg n by A7, A48, ZFMISC_1:87;
then ( i = l implies ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) ) by A37, A49;
hence ((ILine ((1. (K,n)),l,k)) * A) * (i,j) = (ILine (A,l,k)) * (i,j) by A25, A11, A49, A50; :: thesis: verum

end;

A51: ( len ((ILine ((1. (K,n)),l,k)) * A) = n & width ((ILine ((1. (K,n)),l,k)) * A) = n ) by MATRIX_0:24;
( len (ILine (A,l,k)) = len A & width (ILine (A,l,k)) = width A ) by Def1, Th1;
hence (ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k) by A9, A8, A51, A47, MATRIX_0:21; :: thesis: verum