set n = {} ;
let L be non empty doubleLoopStr ; :: thesis: for p being Polynomial of {} ,L ex a being Element of L st p = {(EmptyBag {} )} --> a
let p be Polynomial of {} ,L; :: thesis: ex a being Element of L st p = {(EmptyBag {} )} --> a
A1: for b being bag of {} holds b = {}

proof

let b be bag of {} ; :: thesis: b = {}
b in Bags {} by PRE_POLY:def 12;
hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

end;

reconsider p = p as Function of (Bags {} ),L ;
reconsider p = p as Function of {{} },the carrier of L by PRE_POLY:51;
set a = p /. {} ;
A2: dom p = {{} } by FUNCT_2:def 1
.= {(EmptyBag {} )} by A1 ;
A3: for u being set st u in p holds
u in [:{(EmptyBag {} )},{(p /. {} )}:]

proof

let u be set ; :: thesis: ( u in p implies u in [:{(EmptyBag {} )},{(p /. {} )}:] )
assume A4: u in p ; :: thesis: u in [:{(EmptyBag {} )},{(p /. {} )}:]
then consider p1, p2 being set such that
A5: u = [p1,p2] by RELAT_1:def 1;
A6: p1 in dom p by A4, A5, RELAT_1:def 4;
then reconsider p1 = p1 as bag of {} by A2, TARSKI:def 1;
A7: p1 = {} by A1;
then p2 = p . {} by A4, A5, A6, FUNCT_1:def 4
.= p /. {} by A6, A7, PARTFUN1:def 8 ;
then p2 in {(p /. {} )} by TARSKI:def 1;
hence u in [:{(EmptyBag {} )},{(p /. {} )}:] by A2, A5, A6, ZFMISC_1:def 2; :: thesis: verum

end;

take p /. {} ; :: thesis: p = {(EmptyBag {} )} --> (p /. {} )
A8: EmptyBag {} = {} by A1;
for u being set st u in [:{(EmptyBag {} )},{(p /. {} )}:] holds
u in p

proof

let u be set ; :: thesis: ( u in [:{(EmptyBag {} )},{(p /. {} )}:] implies u in p )
assume u in [:{(EmptyBag {} )},{(p /. {} )}:] ; :: thesis: u in p
then consider u1, u2 being set such that
A9: u1 in {(EmptyBag {} )} and
A10: u2 in {(p /. {} )} and
A11: u = [u1,u2] by ZFMISC_1:def 2;
A12: u1 = {} by A8, A9, TARSKI:def 1;
u2 = p /. {} by A10, TARSKI:def 1
.= p . {} by A2, A9, A12, PARTFUN1:def 8 ;
hence u in p by A2, A9, A11, A12, FUNCT_1:8; :: thesis: verum

end;

hence p = {(EmptyBag {} )} --> (p /. {} ) by A3, TARSKI:2; :: thesis: verum