let D be non empty set ; :: thesis: for m, i, 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 m, i, 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_1:def 8;
then A4: dom (Line (Segm A,nt,mt),i) = Seg m by FINSEQ_1:def 3;
A5: dom mt = Seg m by FINSEQ_2:144;
len (Line A,(nt . i)) = width A by MATRIX_1:def 8;
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:46;

now

let x be set ; :: 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 Element of 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_1:def 8;
[i,k] in [:(Seg n),(Seg (width (Segm A,nt,mt))):] by A1, A3, A4, A7, A8, ZFMISC_1:106;
then A10: [i,k] in Indices (Segm A,nt,mt) by MATRIX_1:26;
mt . k in rng mt by A5, A4, A7, A8, FUNCT_1:def 5;
then A11: (Line A,(nt . i)) . (mt . k) = A * (nt . i),(mt . k) by A2, MATRIX_1:def 8;
((Line A,(nt . i)) * mt) . k = (Line A,(nt . i)) . (mt . k) by A6, A5, A4, A7, A8, FUNCT_1:22;
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, FUNCT_1:9; :: thesis: verum