let L be non empty add-cancelable right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr ; :: thesis: for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
let P be Subset of L; :: thesis: for p being Element of L st p in P holds
p in P -Ideal
let p be Element of L; :: thesis: ( p in P implies p in P -Ideal )
set f = <*p*>;
assume A1: p in P ; :: thesis: p in P -Ideal
then reconsider P9 = P as non empty Subset of L ;

now :: thesis: for i being set st i in dom <*p*> holds
ex u, v being Element of L ex a being Element of P9 st <*p*> /. i = (u * a) * v

let i be set ; :: thesis: ( i in dom <*p*> implies ex u, v being Element of L ex a being Element of P9 st <*p*> /. i = (u * a) * v )
assume A2: i in dom <*p*> ; :: thesis: ex u, v being Element of L ex a being Element of P9 st <*p*> /. i = (u * a) * v
dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by A2, TARSKI:def 1;
then <*p*> /. i = <*p*> . 1 by A2, PARTFUN1:def 6
.= p
.= (1. L) * p
.= ((1. L) * p) * (1. L) ;
hence ex u, v being Element of L ex a being Element of P9 st <*p*> /. i = (u * a) * v by A1; :: thesis: verum

end;

then reconsider f = <*p*> as LinearCombination of P9 by IDEAL_1:def 8;
Sum f = p by RLVECT_1:44;
hence p in P -Ideal by IDEAL_1:60; :: thesis: verum