let n, i be Nat; :: thesis: for K being Field
for A being Matrix of K
for nt being Element of n -tuples_on NAT st i in Seg n holds
Line (Segm A,nt,(Sgm (Seg (width A)))),i = Line A,(nt . i)
let K be Field; :: thesis: for A being Matrix of K
for nt being Element of n -tuples_on NAT st i in Seg n holds
Line (Segm A,nt,(Sgm (Seg (width A)))),i = Line A,(nt . i)
let A be Matrix of K; :: thesis: for nt being Element of n -tuples_on NAT st i in Seg n holds
Line (Segm A,nt,(Sgm (Seg (width A)))),i = Line A,(nt . i)
let nt be Element of n -tuples_on NAT ; :: thesis: ( i in Seg n implies Line (Segm A,nt,(Sgm (Seg (width A)))),i = Line A,(nt . i) )
assume A1: i in Seg n ; :: thesis: Line (Segm A,nt,(Sgm (Seg (width A)))),i = Line A,(nt . i)
set S = Seg (width A);
len (Line A,(nt . i)) = width A by MATRIX_1:def 8;
then ( dom (Line A,(nt . i)) = Seg (width A) & Sgm (Seg (width A)) = idseq (width A) ) by FINSEQ_1:def 3, FINSEQ_3:54;
then ( (Line A,(nt . i)) * (Sgm (Seg (width A))) = Line A,(nt . i) & rng (Sgm (Seg (width A))) = Seg (width A) ) by FINSEQ_1:def 13, RELAT_1:78;
hence Line (Segm A,nt,(Sgm (Seg (width A)))),i = Line A,(nt . i) by A1, MATRIX13:24; :: thesis: verum