let n, m be Nat; :: thesis: for K being Field
for a being Element of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm M,nt,mt) = Segm (a * M),nt,mt
let K be Field; :: thesis: for a being Element of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm M,nt,mt) = Segm (a * M),nt,mt
let a be Element of K; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm M,nt,mt) = Segm (a * M),nt,mt
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm M,nt,mt) = Segm (a * M),nt,mt
let mt be Element of m -tuples_on NAT ; :: thesis: for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm M,nt,mt) = Segm (a * M),nt,mt
let M be Matrix of K; :: thesis: ( [:(rng nt),(rng mt):] c= Indices M implies a * (Segm M,nt,mt) = Segm (a * M),nt,mt )
set Sa = Segm (a * M),nt,mt;
set S = Segm M,nt,mt;
set aS = a * (Segm M,nt,mt);
A1: Indices (a * M) = Indices M by MATRIXR1:18;
A2: Indices (Segm (a * M),nt,mt) = Indices (Segm M,nt,mt) by MATRIX_1:27;
assume A3: [:(rng nt),(rng mt):] c= Indices M ; :: thesis: a * (Segm M,nt,mt) = Segm (a * M),nt,mt

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (a * M),nt,mt) implies (Segm (a * M),nt,mt) * i,j = (a * (Segm M,nt,mt)) * i,j )
assume A4: [i,j] in Indices (Segm (a * M),nt,mt) ; :: thesis: (Segm (a * M),nt,mt) * i,j = (a * (Segm M,nt,mt)) * i,j
A5: (a * (Segm M,nt,mt)) * i,j = a * ((Segm M,nt,mt) * i,j) by A2, A4, MATRIX_3:def 5;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 13;
A6: (Segm (a * M),nt,mt) * i9,j9 = (a * M) * (nt . i),(mt . j) by A4, Def1;
A7: (Segm M,nt,mt) * i9,j9 = M * (nt . i),(mt . j) by A2, A4, Def1;
[(nt . i9),(mt . j9)] in Indices M by A3, A1, A4, Th17;
hence (Segm (a * M),nt,mt) * i,j = (a * (Segm M,nt,mt)) * i,j by A6, A5, A7, MATRIX_3:def 5; :: thesis: verum

end;

hence a * (Segm M,nt,mt) = Segm (a * M),nt,mt by MATRIX_1:28; :: thesis: verum