set n = {} ;
let L be non empty doubleLoopStr ; for p being Polynomial of {},L ex a being Element of L st p = {(EmptyBag {})} --> a
let p be Polynomial of {},L; ex a being Element of L st p = {(EmptyBag {})} --> a
A1:
for b being bag of {} holds b = {}
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 object st u in p holds
u in [:{(EmptyBag {})},{(p /. {})}:]
proof
let u be
object ;
( u in p implies u in [:{(EmptyBag {})},{(p /. {})}:] )
assume A4:
u in p
;
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;
verum
end;
take
p /. {}
; p = {(EmptyBag {})} --> (p /. {})
A9:
EmptyBag {} = {}
by A1;
for u being object st u in [:{(EmptyBag {})},{(p /. {})}:] holds
u in p
proof
let u be
object ;
( u in [:{(EmptyBag {})},{(p /. {})}:] implies u in p )
assume
u in [:{(EmptyBag {})},{(p /. {})}:]
;
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;
verum
end;
hence
p = {(EmptyBag {})} --> (p /. {})
by A3, TARSKI:2; verum