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 ;

Sum f = p by RLVECT_1:44;

hence p in P -Ideal by IDEAL_1:60; :: thesis: verum

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

then reconsider f = <*p*> as LinearCombination of P9 by IDEAL_1:def 8;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 by FINSEQ_1:40

.= (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;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 by FINSEQ_1:40

.= (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

Sum f = p by RLVECT_1:44;

hence p in P -Ideal by IDEAL_1:60; :: thesis: verum