let D be non empty set ; :: thesis: for i, m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt
let i, m, n be Nat; :: thesis: for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt
let A be Matrix of D; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt
let nt be Element of n -tuples_on NAT; :: thesis: for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt
let mt be Element of m -tuples_on NAT; :: thesis: ( i in Seg n & rng mt c= Seg (width A) implies Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt )
set S = Segm (A,nt,mt);
set Li = Line ((Segm (A,nt,mt)),i);
set LA = Line (A,(nt . i));
assume that
A1: i in Seg n and
A2: rng mt c= Seg (width A) ; :: thesis: Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt
n <> 0 by A1;
then A3: width (Segm (A,nt,mt)) = m by Th1;
then len (Line ((Segm (A,nt,mt)),i)) = m by MATRIX_0:def 7;
then A4: dom (Line ((Segm (A,nt,mt)),i)) = Seg m by FINSEQ_1:def 3;
A5: dom mt = Seg m by FINSEQ_2:124;
len (Line (A,(nt . i))) = width A by MATRIX_0:def 7;
then dom (Line (A,(nt . i))) = Seg (width A) by FINSEQ_1:def 3;
then A6: dom ((Line (A,(nt . i))) * mt) = dom mt by A2, RELAT_1:27;

now :: thesis: for x being object st x in dom (Line ((Segm (A,nt,mt)),i)) holds
(Line ((Segm (A,nt,mt)),i)) . x = ((Line (A,(nt . i))) * mt) . x

let x be object ; :: thesis: ( x in dom (Line ((Segm (A,nt,mt)),i)) implies (Line ((Segm (A,nt,mt)),i)) . x = ((Line (A,(nt . i))) * mt) . x )
assume A7: x in dom (Line ((Segm (A,nt,mt)),i)) ; :: thesis: (Line ((Segm (A,nt,mt)),i)) . x = ((Line (A,(nt . i))) * mt) . x
consider k being Nat such that
A8: k = x and
1 <= k and
k <= m by A4, A7;
A9: (Line ((Segm (A,nt,mt)),i)) . k = (Segm (A,nt,mt)) * (i,k) by A3, A4, A7, A8, MATRIX_0:def 7;
[i,k] in [:(Seg n),(Seg (width (Segm (A,nt,mt)))):] by A1, A3, A4, A7, A8, ZFMISC_1:87;
then A10: [i,k] in Indices (Segm (A,nt,mt)) by MATRIX_0:25;
mt . k in rng mt by A5, A4, A7, A8, FUNCT_1:def 3;
then A11: (Line (A,(nt . i))) . (mt . k) = A * ((nt . i),(mt . k)) by A2, MATRIX_0:def 7;
((Line (A,(nt . i))) * mt) . k = (Line (A,(nt . i))) . (mt . k) by A6, A5, A4, A7, A8, FUNCT_1:12;
hence (Line ((Segm (A,nt,mt)),i)) . x = ((Line (A,(nt . i))) * mt) . x by A8, A11, A10, A9, Def1; :: thesis: verum

end;

hence Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt by A6, A5, A4; :: thesis: verum