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
set n = {} ;
A1:
for b being bag of holds b = {}
then A2:
EmptyBag {} = {}
;
reconsider p = p as Function of (Bags {} ),L ;
reconsider p = p as Function of {{} },the carrier of L by POLYNOM1:55;
A3: dom p =
{{} }
by FUNCT_2:def 1
.=
{(EmptyBag {} )}
by A1
;
set a = p /. {} ;
take
p /. {}
; :: thesis: p = {(EmptyBag {} )} --> (p /. {} )
A4:
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 A5:
u in p
;
:: thesis: u in [:{(EmptyBag {} )},{(p /. {} )}:]
then consider p1,
p2 being
set such that A6:
u = [p1,p2]
by RELAT_1:def 1;
A7:
(
p1 in dom p &
p2 in rng p )
by A5, A6, RELAT_1:def 4, RELAT_1:def 5;
then reconsider p1 =
p1 as
bag of
by A3, TARSKI:def 1;
A8:
p1 = {}
by A1;
then p2 =
p . {}
by A5, A6, A7, FUNCT_1:def 4
.=
p /. {}
by A7, A8, PARTFUN1:def 8
;
then
p2 in {(p /. {} )}
by TARSKI:def 1;
hence
u in [:{(EmptyBag {} )},{(p /. {} )}:]
by A3, A6, A7, ZFMISC_1:def 2;
:: thesis: verum
end;
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 {} )} &
u2 in {(p /. {} )} &
u = [u1,u2] )
by ZFMISC_1:def 2;
A10:
u1 = {}
by A2, A9, TARSKI:def 1;
u2 =
p /. {}
by A9, TARSKI:def 1
.=
p . {}
by A3, A9, A10, PARTFUN1:def 8
;
hence
u in p
by A3, A9, A10, FUNCT_1:8;
:: thesis: verum
end;
hence
p = {(EmptyBag {} )} --> (p /. {} )
by A4, TARSKI:2; :: thesis: verum