theorem Th4:
for
l,
n,
m,
i being
Nat for
K being
Field for
a being
Element of
K for
M,
M1 being
Matrix of
n,
m,
K st
l in dom M &
i in dom M &
M1 = ScalarXLine (
M,
l,
a) holds
( (
i = l implies
Line (
M1,
i)
= a * (Line (M,l)) ) & (
i <> l implies
Line (
M1,
i)
= Line (
M,
i) ) )