let L be non empty add-cancelable right_complementable associative well-unital distributive add-associative right_zeroed 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 )
assume A1: p in P ; :: thesis: p in P -Ideal
then reconsider P' = P as non empty Subset of L ;
set f = <*p*>;

now

let i be set ; :: thesis: ( i in dom <*p*> implies ex u, v being Element of L ex a being Element of P' 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 P' st <*p*> /. i = (u * a) * v
dom <*p*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then i = 1 by A2, TARSKI:def 1;
then <*p*> /. i = <*p*> . 1 by A2, PARTFUN1:def 8
.= p by FINSEQ_1:57
.= (1. L) * p by VECTSP_1:def 19
.= ((1. L) * p) * (1. L) by VECTSP_1:def 13 ;
hence ex u, v being Element of L ex a being Element of P' st <*p*> /. i = (u * a) * v by A1; :: thesis: verum

end;

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