let X be non empty set ; :: thesis: for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds
( ex x being Element of X st Support (@ f) = {x} iff len (idxseq f) = 1 )
let R be non degenerated Ring; :: thesis: for f being Element of (Free_LMod (X,R)) holds
( ex x being Element of X st Support (@ f) = {x} iff len (idxseq f) = 1 )
let f be Element of (Free_LMod (X,R)); :: thesis: ( ex x being Element of X st Support (@ f) = {x} iff len (idxseq f) = 1 )
thus ( ex x being Element of X st Support (@ f) = {x} implies len (idxseq f) = 1 ) :: thesis: ( len (idxseq f) = 1 implies ex x being Element of X st Support (@ f) = {x} )

proof

given x being Element of X such that A1: Support (@ f) = {x} ; :: thesis: len (idxseq f) = 1
card (canFS (Support (@ f))) = card (Support (@ f)) by FINSEQ_1:93
.= 1 by A1, CARD_1:30 ;
hence len (idxseq f) = 1 ; :: thesis: verum

end;

assume len (idxseq f) = 1 ; :: thesis: ex x being Element of X st Support (@ f) = {x}
then card (Support (@ f)) = 1 by FINSEQ_1:93;
then consider a being object such that
A4: Support (@ f) = {a} by CARD_2:42;
reconsider x = a as Element of X by A4, ZFMISC_1:31;
take x ; :: thesis: Support (@ f) = {x}
thus Support (@ f) = {x} by A4; :: thesis: verum