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;

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

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 )

assume
( r <> 0 or Av is trivial )
; :: thesis: r (#) EV is Enumeration of r * Avreconsider 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 (#) 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

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