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 )
assume A1: [:(rng nt),(rng mt):] c= Indices M ; :: thesis: 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);
A2: ( Indices (a * M) = Indices M & Indices (Segm (a * M),nt,mt) = Indices (Segm M,nt,mt) ) by MATRIXR1:18, MATRIX_1:27;

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 A3: [i,j] in Indices (Segm (a * M),nt,mt) ; :: thesis: (Segm (a * M),nt,mt) * i,j = (a * (Segm M,nt,mt)) * i,j
reconsider i' = i, j' = j as Element of NAT by ORDINAL1:def 13;
( (Segm (a * M),nt,mt) * i',j' = (a * M) * (nt . i),(mt . j) & [(nt . i'),(mt . j')] in Indices M & (a * (Segm M,nt,mt)) * i,j = a * ((Segm M,nt,mt) * i,j) & (Segm M,nt,mt) * i',j' = M * (nt . i),(mt . j) ) by A1, A2, A3, Def1, Th17, MATRIX_3:def 5;
hence (Segm (a * M),nt,mt) * i,j = (a * (Segm M,nt,mt)) * i,j by MATRIX_3:def 5; :: thesis: verum

end;

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