let X be non empty set ; :: thesis: for R being non degenerated Ring
for f being Element of (Free_LMod (X,R)) holds f = Sum (F_idxseq f)
let R be non degenerated Ring; :: thesis: for f being Element of (Free_LMod (X,R)) holds f = Sum (F_idxseq f)
let f be Element of (Free_LMod (X,R)); :: thesis: f = Sum (F_idxseq f)
A1: dom (@ f) = X by FUNCT_2:def 1
.= dom (@ (Sum (F_idxseq f))) by FUNCT_2:def 1 ;
for o being object st o in dom (@ f) holds
(@ f) . o = (@ (Sum (F_idxseq f))) . o

proof

let o be object ; :: thesis: ( o in dom (@ f) implies (@ f) . o = (@ (Sum (F_idxseq f))) . o )
assume o in dom (@ f) ; :: thesis: (@ f) . o = (@ (Sum (F_idxseq f))) . o
then reconsider x = o as Element of X ;

per cases ( o in Support (@ f) or not o in Support (@ f) ) ;

suppose o in Support (@ f) ; :: thesis: (@ f) . o = (@ (Sum (F_idxseq f))) . o

hence (@ f) . o = (@ (Sum (F_idxseq f))) . o by Th14; :: thesis: verum

end;

suppose A4: not o in Support (@ f) ; :: thesis: (@ f) . o = (@ (Sum (F_idxseq f))) . o

(@ f) . x = (ev_ (x,R)) . f by Def20
.= 0. R by A4, Lm18
.= (@ (Sum (F_idxseq f))) . x by A4, Th12 ;
hence (@ f) . o = (@ (Sum (F_idxseq f))) . o ; :: thesis: verum

end;

end;

end;

then @ f = @ (Sum (F_idxseq f)) by A1;
hence f = Sum (F_idxseq f) ; :: thesis: verum