let r be Real; :: thesis: for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )

let V be RealLinearSpace; :: thesis: for Av being finite Subset of V
for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )

let Av be finite Subset of V; :: thesis: for E being Enumeration of Av holds
( r (#) E is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )

let EV be Enumeration of Av; :: thesis: ( r (#) EV is Enumeration of r * Av iff ( r <> 0 or Av is trivial ) )
set rE = r (#) EV;
A1: dom (r (#) EV) = dom EV by VFUNCT_1:def 4;
then A2: len (r (#) EV) = len EV by FINSEQ_3:29;
A3: rng EV = Av by Def1;
then A4: card Av = len EV by FINSEQ_4:62;
A5: rng (r (#) EV) = (r (#) EV) .: (dom EV) by
.= r * (EV .: (dom EV)) by Th10
.= r * Av by ;
A6: card {(0. V)} = 1 by CARD_2:42;
hereby :: thesis: ( ( r <> 0 or Av is trivial ) implies r (#) EV is Enumeration of r * Av )
reconsider rA = r * Av as finite set ;
assume r (#) EV is Enumeration of r * Av ; :: thesis: ( r = 0 implies Av is trivial )
then A7: card (r * Av) = card Av by ;
assume r = 0 ; :: thesis: Av is trivial
then card Av <= 1 by ;
then card Av < 1 + 1 by NAT_1:13;
hence Av is trivial by NAT_D:60; :: thesis: verum
end;
assume ( r <> 0 or Av is trivial ) ; :: thesis: r (#) EV is Enumeration of r * Av
then card Av = card (r * Av) by Th12;
then r (#) EV is one-to-one by ;
hence r (#) EV is Enumeration of r * Av by ; :: thesis: verum