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 A1, RELAT_1:113
.= r * (EV .: (dom EV)) by Th10
.= r * Av by A3, RELAT_1:113 ;
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 A4, A2, A5, FINSEQ_4:62;
assume r = 0 ; :: thesis: Av is trivial
then card Av <= 1 by A6, A7, NAT_1:43, RLAFFIN1:12;
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 A4, A2, A5, FINSEQ_4:62;
hence r (#) EV is Enumeration of r * Av by A5, Def1; :: thesis: verum