set n = {} ;
let L be non empty doubleLoopStr ; :: thesis: for p being Polynomial of {},L ex a being Element of L st p = {()} --> a
let p be Polynomial of {},L; :: thesis: ex a being Element of L st p = {()} --> 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 ; :: thesis: verum
end;
reconsider p = p as Function of (),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
.= {()} by A1 ;
A3: for u being object st u in p holds
u in [:{()},{(p /. {})}:]
proof
let u be object ; :: thesis: ( u in p implies u in [:{()},{(p /. {})}:] )
assume A4: u in p ; :: thesis: u in [:{()},{(p /. {})}:]
then consider p1, p2 being object such that
A5: u = [p1,p2] by RELAT_1:def 1;
A6: p1 in dom p by ;
then reconsider p1 = p1 as bag of {} by A2;
A7: p2 is set by TARSKI:1;
A8: p1 = {} by A1;
then p2 = p . {} by
.= p /. {} by ;
then p2 in {(p /. {})} by TARSKI:def 1;
hence u in [:{()},{(p /. {})}:] by ; :: thesis: verum
end;
take p /. {} ; :: thesis: p = {()} --> (p /. {})
A9: EmptyBag {} = {} by A1;
for u being object st u in [:{()},{(p /. {})}:] holds
u in p
proof
let u be object ; :: thesis: ( u in [:{()},{(p /. {})}:] implies u in p )
assume u in [:{()},{(p /. {})}:] ; :: thesis: u in p
then consider u1, u2 being object such that
A10: u1 in {()} and
A11: u2 in {(p /. {})} and
A12: u = [u1,u2] by ZFMISC_1:def 2;
A13: u1 = {} by ;
u2 = p /. {} by
.= p . {} by ;
hence u in p by ; :: thesis: verum
end;
hence p = {()} --> (p /. {}) by ; :: thesis: verum