theorem Th15: :: RLAFFIN3:15

for n, m being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A