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 = {}

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 object st u in p holds

u in [:{(EmptyBag {})},{(p /. {})}:]

A9: EmptyBag {} = {} by A1;

for u being object st u in [:{(EmptyBag {})},{(p /. {})}:] holds

u in p

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

reconsider p = p as Function of (Bags {}),L ;
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;b in Bags {} by PRE_POLY:def 12;

hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

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 object st u in p holds

u in [:{(EmptyBag {})},{(p /. {})}:]

proof

take
p /. {}
; :: thesis: p = {(EmptyBag {})} --> (p /. {})
let u be object ; :: thesis: ( u in p implies u in [:{(EmptyBag {})},{(p /. {})}:] )

assume A4: u in p ; :: thesis: u in [:{(EmptyBag {})},{(p /. {})}:]

then consider p1, p2 being object such that

A5: u = [p1,p2] by RELAT_1:def 1;

A6: p1 in dom p by A4, A5, XTUPLE_0:def 12;

then reconsider p1 = p1 as bag of {} by A2;

A7: p2 is set by TARSKI:1;

A8: p1 = {} by A1;

then p2 = p . {} by A4, A5, A6, FUNCT_1:def 2, A7

.= p /. {} by A6, A8, PARTFUN1:def 6 ;

then p2 in {(p /. {})} by TARSKI:def 1;

hence u in [:{(EmptyBag {})},{(p /. {})}:] by A2, A5, A6, ZFMISC_1:def 2; :: thesis: verum

end;assume A4: u in p ; :: thesis: u in [:{(EmptyBag {})},{(p /. {})}:]

then consider p1, p2 being object such that

A5: u = [p1,p2] by RELAT_1:def 1;

A6: p1 in dom p by A4, A5, XTUPLE_0:def 12;

then reconsider p1 = p1 as bag of {} by A2;

A7: p2 is set by TARSKI:1;

A8: p1 = {} by A1;

then p2 = p . {} by A4, A5, A6, FUNCT_1:def 2, A7

.= p /. {} by A6, A8, PARTFUN1:def 6 ;

then p2 in {(p /. {})} by TARSKI:def 1;

hence u in [:{(EmptyBag {})},{(p /. {})}:] by A2, A5, A6, ZFMISC_1:def 2; :: thesis: verum

A9: EmptyBag {} = {} by A1;

for u being object st u in [:{(EmptyBag {})},{(p /. {})}:] holds

u in p

proof

hence
p = {(EmptyBag {})} --> (p /. {})
by A3, TARSKI:2; :: thesis: verum
let u be object ; :: thesis: ( u in [:{(EmptyBag {})},{(p /. {})}:] implies u in p )

assume u in [:{(EmptyBag {})},{(p /. {})}:] ; :: thesis: u in p

then consider u1, u2 being object such that

A10: u1 in {(EmptyBag {})} and

A11: u2 in {(p /. {})} and

A12: u = [u1,u2] by ZFMISC_1:def 2;

A13: u1 = {} by A9, A10, TARSKI:def 1;

u2 = p /. {} by A11, TARSKI:def 1

.= p . {} by A2, A10, A13, PARTFUN1:def 6 ;

hence u in p by A2, A10, A12, A13, FUNCT_1:1; :: thesis: verum

end;assume u in [:{(EmptyBag {})},{(p /. {})}:] ; :: thesis: u in p

then consider u1, u2 being object such that

A10: u1 in {(EmptyBag {})} and

A11: u2 in {(p /. {})} and

A12: u = [u1,u2] by ZFMISC_1:def 2;

A13: u1 = {} by A9, A10, TARSKI:def 1;

u2 = p /. {} by A11, TARSKI:def 1

.= p . {} by A2, A10, A13, PARTFUN1:def 6 ;

hence u in p by A2, A10, A12, A13, FUNCT_1:1; :: thesis: verum