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
A3: ( len (Line A,(nt . i)) = width A & width (Segm A,nt,mt) = m ) by A1, Th1, FINSEQ_1:4, MATRIX_1:def 8;
then ( dom (Line A,(nt . i)) = Seg (width A) & len (Line (Segm A,nt,mt),i) = m ) by FINSEQ_1:def 3, MATRIX_1:def 8;
then A4: ( dom ((Line A,(nt . i)) * mt) = dom mt & dom mt = Seg m & dom (Line (Segm A,nt,mt),i) = Seg m ) by A2, FINSEQ_1:def 3, FINSEQ_2:144, 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 A5: 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
A6: ( k = x & 1 <= k & k <= m ) by A4, A5;
( mt . k in rng mt & [i,k] in [:(Seg n),(Seg (width (Segm A,nt,mt))):] ) by A1, A3, A4, A5, A6, FUNCT_1:def 5, ZFMISC_1:106;
then ( ((Line A,(nt . i)) * mt) . k = (Line A,(nt . i)) . (mt . k) & (Line A,(nt . i)) . (mt . k) = A * (nt . i),(mt . k) & [i,k] in Indices (Segm A,nt,mt) & (Line (Segm A,nt,mt),i) . k = (Segm A,nt,mt) * i,k ) by A2, A3, A4, A5, A6, FUNCT_1:22, MATRIX_1:26, MATRIX_1:def 8;
hence (Line (Segm A,nt,mt),i) . x = ((Line A,(nt . i)) * mt) . x by A6, Def1; :: thesis: verum

end;

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