let X be non empty set ; :: thesis: for R being non degenerated Ring
for x being Element of X
for f being Element of (Free_LMod (X,R)) st Support (@ f) = {x} holds
( f = ((@ f) . x) * ((IotaMap (X,R)) . x) & f = (F_idxseq f) . 1 & F_idxseq f = <*((F_idxseq f) . 1)*> & idxseq f = <*x*> )
let R be non degenerated Ring; :: thesis: for x being Element of X
for f being Element of (Free_LMod (X,R)) st Support (@ f) = {x} holds
( f = ((@ f) . x) * ((IotaMap (X,R)) . x) & f = (F_idxseq f) . 1 & F_idxseq f = <*((F_idxseq f) . 1)*> & idxseq f = <*x*> )
let x be Element of X; :: thesis: for f being Element of (Free_LMod (X,R)) st Support (@ f) = {x} holds
( f = ((@ f) . x) * ((IotaMap (X,R)) . x) & f = (F_idxseq f) . 1 & F_idxseq f = <*((F_idxseq f) . 1)*> & idxseq f = <*x*> )
let f be Element of (Free_LMod (X,R)); :: thesis: ( Support (@ f) = {x} implies ( f = ((@ f) . x) * ((IotaMap (X,R)) . x) & f = (F_idxseq f) . 1 & F_idxseq f = <*((F_idxseq f) . 1)*> & idxseq f = <*x*> ) )
assume A1: Support (@ f) = {x} ; :: thesis: ( f = ((@ f) . x) * ((IotaMap (X,R)) . x) & f = (F_idxseq f) . 1 & F_idxseq f = <*((F_idxseq f) . 1)*> & idxseq f = <*x*> )
then consider x0 being Element of X such that
A2: Support (@ f) = {x0} ;
A4: x = x0 by A1, A2, ZFMISC_1:3;
A5: len (idxseq f) = 1 by A2, Lm25;
dom (F_idxseq f) = Seg (len (F_idxseq f)) by FINSEQ_1:def 3
.= Seg 1 by A5, Def24 ;
then A6: 1 in dom (F_idxseq f) ;
A7: idxseq f = <*x0*> by A2, FINSEQ_1:94;
A8: (F_idxseq f) . 1 = (ev_iota f) . ((idxseq f) . 1) by A6, Def24
.= ((ev_ (x0,R)) . f) * ((IotaMap (X,R)) . x0) by A7, Def21
.= ((@ f) . x) * ((IotaMap (X,R)) . x) by A4, Def20 ;
then F_idxseq f = <*(((@ f) . x) * ((IotaMap (X,R)) . x))*> by A5, Def24, FINSEQ_1:40;
then f = Sum <*(((@ f) . x) * ((IotaMap (X,R)) . x))*> by Th15;
hence ( f = ((@ f) . x) * ((IotaMap (X,R)) . x) & f = (F_idxseq f) . 1 & F_idxseq f = <*((F_idxseq f) . 1)*> & idxseq f = <*x*> ) by RLVECT_1:44, A8, A5, Def24, FINSEQ_1:40, FINSEQ_1:94, A1; :: thesis: verum