let i, n 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)) )

set S = Seg (width A);

A1: rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 13;

len (Line (A,(nt . i))) = width A by MATRIX_0:def 7;

then A2: dom (Line (A,(nt . i))) = Seg (width A) by FINSEQ_1:def 3;

Sgm (Seg (width A)) = idseq (width A) by FINSEQ_3:48;

then A3: (Line (A,(nt . i))) * (Sgm (Seg (width A))) = Line (A,(nt . i)) by A2, RELAT_1:52;

assume i in Seg n ; :: thesis: Line ((Segm (A,nt,(Sgm (Seg (width A))))),i) = Line (A,(nt . i))

hence Line ((Segm (A,nt,(Sgm (Seg (width A))))),i) = Line (A,(nt . i)) by A3, A1, MATRIX13:24; :: thesis: verum

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)) )

set S = Seg (width A);

A1: rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 13;

len (Line (A,(nt . i))) = width A by MATRIX_0:def 7;

then A2: dom (Line (A,(nt . i))) = Seg (width A) by FINSEQ_1:def 3;

Sgm (Seg (width A)) = idseq (width A) by FINSEQ_3:48;

then A3: (Line (A,(nt . i))) * (Sgm (Seg (width A))) = Line (A,(nt . i)) by A2, RELAT_1:52;

assume i in Seg n ; :: thesis: Line ((Segm (A,nt,(Sgm (Seg (width A))))),i) = Line (A,(nt . i))

hence Line ((Segm (A,nt,(Sgm (Seg (width A))))),i) = Line (A,(nt . i)) by A3, A1, MATRIX13:24; :: thesis: verum