let m, n 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_0:26;
assume A3: [:(rng nt),(rng mt):] c= Indices M ; :: thesis: a * (Segm (M,nt,mt)) = Segm ((a * M),nt,mt)

now :: thesis: for i, j being Nat st [i,j] in Indices (Segm ((a * M),nt,mt)) holds
(Segm ((a * M),nt,mt)) * (i,j) = (a * (Segm (M,nt,mt))) * (i,j)

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 12;
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_0:27; :: thesis: verum