:: ZFMODEL2 semantic presentation

REAL is set
NAT is non empty V19() V20() V21() Element of K27(REAL)
K27(REAL) is set
NAT is non empty V19() V20() V21() set
K27(NAT) is set
K27(NAT) is set
VAR is non empty Element of K27(NAT)
K27(VAR) is set
1 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
2 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
3 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
0 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
the Function-like functional empty ext-real non positive non negative V18() V19() V20() V21() V23() V24() V25() V26() finite V37() V43() set is Function-like functional empty ext-real non positive non negative V18() V19() V20() V21() V23() V24() V25() V26() finite V37() V43() set
{} is set
x. 0 is Element of VAR
x. 3 is Element of VAR
4 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
x. 4 is Element of VAR

{(x. 3),(x. 4)} is finite set
{0,1,2,3,4} is finite set
M is Element of VAR
{M} is finite set
H is Element of VAR
{H} is finite set

Free (i / (M,H)) is Element of K27(VAR)
Free i is Element of K27(VAR)
(Free i) \ {M} is Element of K27(VAR)
((Free i) \ {M}) \/ {H} is set
v is Element of VAR
a is Element of VAR

Free ((v '=' a) / (M,H)) is Element of K27(VAR)
Free (v '=' a) is Element of K27(VAR)
(Free (v '=' a)) \ {M} is Element of K27(VAR)
((Free (v '=' a)) \ {M}) \/ {H} is set

Free ((v 'in' a) / (M,H)) is Element of K27(VAR)
Free (v 'in' a) is Element of K27(VAR)
(Free (v 'in' a)) \ {M} is Element of K27(VAR)
((Free (v 'in' a)) \ {M}) \/ {H} is set
m4 is Element of VAR
f is Element of VAR
{m4,f} is finite set
{v,a} is finite set
{v,a} \ {M} is finite Element of K27({v,a})
K27({v,a}) is finite V37() set
({v,a} \ {M}) \/ {H} is finite set
p is set

Free (v / (M,H)) is Element of K27(VAR)
Free v is Element of K27(VAR)
(Free v) \ {M} is Element of K27(VAR)
((Free v) \ {M}) \/ {H} is set

Free (a / (M,H)) is Element of K27(VAR)
Free a is Element of K27(VAR)
(Free a) \ {M} is Element of K27(VAR)
((Free a) \ {M}) \/ {H} is set

Free ((v '&' a) / (M,H)) is Element of K27(VAR)
Free (v '&' a) is Element of K27(VAR)
(Free (v '&' a)) \ {M} is Element of K27(VAR)
((Free (v '&' a)) \ {M}) \/ {H} is set
(v / (M,H)) '&' (a / (M,H)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v / (M,H)) '&' (a / (M,H))) is Element of K27(VAR)
(Free (v / (M,H))) \/ (Free (a / (M,H))) is Element of K27(VAR)
(((Free v) \ {M}) \/ {H}) \/ (((Free a) \ {M}) \/ {H}) is set
(Free v) \/ (Free a) is Element of K27(VAR)
((Free v) \/ (Free a)) \ {M} is Element of K27(VAR)
(((Free v) \/ (Free a)) \ {M}) \/ {H} is set
m4 is set

Free (v / (M,H)) is Element of K27(VAR)
Free v is Element of K27(VAR)
(Free v) \ {M} is Element of K27(VAR)
((Free v) \ {M}) \/ {H} is set
a is Element of VAR

(All (a,v)) / (M,H) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((All (a,v)) / (M,H)) is Element of K27(VAR)
Free (All (a,v)) is Element of K27(VAR)
(Free (All (a,v))) \ {M} is Element of K27(VAR)
((Free (All (a,v))) \ {M}) \/ {H} is set
{a} is finite set
(Free v) \ {a} is Element of K27(VAR)
m4 is Element of VAR
{m4} is finite set
(((Free v) \ {M}) \/ {H}) \ {m4} is Element of K27((((Free v) \ {M}) \/ {H}))
K27((((Free v) \ {M}) \/ {H})) is set
((Free v) \ {a}) \ {M} is Element of K27(VAR)
(((Free v) \ {a}) \ {M}) \/ {H} is set
f is set
(Free (v / (M,H))) \ {m4} is Element of K27(VAR)
All (m4,(v / (M,H))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (All (m4,(v / (M,H)))) is Element of K27(VAR)

Free (v / (M,H)) is Element of K27(VAR)
Free v is Element of K27(VAR)
(Free v) \ {M} is Element of K27(VAR)
((Free v) \ {M}) \/ {H} is set

Free (() / (M,H)) is Element of K27(VAR)
Free () is Element of K27(VAR)
(Free ()) \ {M} is Element of K27(VAR)
((Free ()) \ {M}) \/ {H} is set

Free ('not' (v / (M,H))) is Element of K27(VAR)
M is Element of VAR
{M} is finite set
H is Element of VAR
{H} is finite set

variables_in i is non empty Element of K27(VAR)
Free i is Element of K27(VAR)

Free (i / (H,M)) is Element of K27(VAR)
(Free i) \ {H} is Element of K27(VAR)
((Free i) \ {H}) \/ {M} is set

variables_in v is non empty Element of K27(VAR)
Free v is Element of K27(VAR)

Free (v / (H,M)) is Element of K27(VAR)
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set

variables_in a is non empty Element of K27(VAR)
Free a is Element of K27(VAR)

Free (a / (H,M)) is Element of K27(VAR)
(Free a) \ {H} is Element of K27(VAR)
((Free a) \ {H}) \/ {M} is set

variables_in (v '&' a) is non empty Element of K27(VAR)
Free (v '&' a) is Element of K27(VAR)

Free ((v '&' a) / (H,M)) is Element of K27(VAR)
(Free (v '&' a)) \ {H} is Element of K27(VAR)
((Free (v '&' a)) \ {H}) \/ {M} is set
(v / (H,M)) '&' (a / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((v / (H,M)) '&' (a / (H,M))) is Element of K27(VAR)
(Free (v / (H,M))) \/ (Free (a / (H,M))) is Element of K27(VAR)
(Free v) \/ (Free a) is Element of K27(VAR)
() \/ () is Element of K27(VAR)
((Free v) \ {H}) \/ ((Free a) \ {H}) is Element of K27(VAR)
(((Free v) \ {H}) \/ ((Free a) \ {H})) \/ {M} is set
{M} \/ ((Free v) \ {H}) is set
({M} \/ ((Free v) \ {H})) \/ ((Free a) \ {H}) is set
(({M} \/ ((Free v) \ {H})) \/ ((Free a) \ {H})) \/ {M} is set
{M} \/ (((Free v) \ {H}) \/ ((Free a) \ {H})) is set
({M} \/ (((Free v) \ {H}) \/ ((Free a) \ {H}))) \/ {M} is set
(((Free (v '&' a)) \ {H}) \/ {M}) \/ {M} is set
{M} \/ {M} is finite set
((Free (v '&' a)) \ {H}) \/ ({M} \/ {M}) is set

variables_in v is non empty Element of K27(VAR)
Free v is Element of K27(VAR)

Free (v / (H,M)) is Element of K27(VAR)
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set
a is Element of VAR

variables_in (All (a,v)) is non empty Element of K27(VAR)
Free (All (a,v)) is Element of K27(VAR)
(All (a,v)) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free ((All (a,v)) / (H,M)) is Element of K27(VAR)
(Free (All (a,v))) \ {H} is Element of K27(VAR)
((Free (All (a,v))) \ {H}) \/ {M} is set
{a} is finite set
(Free v) \ {a} is Element of K27(VAR)
f is Element of VAR
All (f,(v / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Free (All (f,(v / (H,M)))) is Element of K27(VAR)
{f} is finite set
(Free (v / (H,M))) \ {f} is Element of K27(VAR)
() \/ {a} is set
p is set
p is set
p is set
((Free v) \ {a}) \/ {M} is set
p is set
((Free v) \ {a}) \ {M} is Element of K27(VAR)
v is Element of VAR
a is Element of VAR

variables_in (v '=' a) is non empty Element of K27(VAR)
Free (v '=' a) is Element of K27(VAR)

Free ((v '=' a) / (H,M)) is Element of K27(VAR)
(Free (v '=' a)) \ {H} is Element of K27(VAR)
((Free (v '=' a)) \ {H}) \/ {M} is set

variables_in (v 'in' a) is non empty Element of K27(VAR)
Free (v 'in' a) is Element of K27(VAR)

Free ((v 'in' a) / (H,M)) is Element of K27(VAR)
(Free (v 'in' a)) \ {H} is Element of K27(VAR)
((Free (v 'in' a)) \ {H}) \/ {M} is set
m4 is Element of VAR
f is Element of VAR

{m4,f} is finite set
{v,a} is finite set
p is set

p is set

variables_in v is non empty Element of K27(VAR)
Free v is Element of K27(VAR)

Free (v / (H,M)) is Element of K27(VAR)
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set

variables_in () is non empty Element of K27(VAR)
Free () is Element of K27(VAR)

Free (() / (H,M)) is Element of K27(VAR)
(Free ()) \ {H} is Element of K27(VAR)
((Free ()) \ {H}) \/ {M} is set

Free ('not' (v / (H,M))) is Element of K27(VAR)

variables_in M is non empty Element of K27(VAR)
rng M is finite set
(rng M) \ {0,1,2,3,4} is finite Element of K27((rng M))
K27((rng M)) is finite V37() set

variables_in M is non empty finite Element of K27(VAR)
H is Element of VAR
i is Element of VAR

variables_in (H '=' i) is non empty finite Element of K27(VAR)

variables_in (H 'in' i) is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. v is Element of VAR
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR
a + v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
v + a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
(v + a) + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
{H,i} is finite set
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. m4 is Element of VAR
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. m4 is Element of VAR

variables_in H is non empty finite Element of K27(VAR)

variables_in i is non empty finite Element of K27(VAR)

variables_in (H '&' i) is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
f is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. f is Element of VAR
() \/ () is finite Element of K27(VAR)

variables_in H is non empty finite Element of K27(VAR)
i is Element of VAR

variables_in (All (i,H)) is non empty finite Element of K27(VAR)
v is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR
a + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
m4 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
f is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. f is Element of VAR
{i} is finite set
() \/ {i} is finite set
a + 0 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT

variables_in H is non empty finite Element of K27(VAR)

variables_in () is non empty finite Element of K27(VAR)
i is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
H is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. H is Element of VAR
M is Element of VAR
H is non empty set
K28(VAR,H) is set
K27(K28(VAR,H)) is set

variables_in i is non empty finite Element of K27(VAR)

v is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
Free i is Element of K27(VAR)
v . M is Element of H
v / (M,(v . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
M is Element of VAR
H is non empty set
K28(VAR,H) is set
K27(K28(VAR,H)) is set
i is Element of H

variables_in v is non empty finite Element of K27(VAR)
a is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a / (M,i) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))

a . M is Element of H
(a / (M,i)) / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
M is Element of VAR
H is Element of VAR
i is Element of VAR
v is non empty set
K28(VAR,v) is set
K27(K28(VAR,v)) is set
a is Element of v
m4 is Element of v
f is Element of v
p is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
p / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (M,a)) / (H,m4) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
((p / (M,a)) / (H,m4)) / (i,f) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
p / (i,f) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (i,f)) / (H,m4) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
((p / (i,f)) / (H,m4)) / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
p / (H,m4) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (H,m4)) / (i,f) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
((p / (H,m4)) / (i,f)) / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
(p / (H,m4)) / (M,a) is Relation-like VAR -defined v -valued Function-like non empty V14( VAR ) V30( VAR ,v) Element of K27(K28(VAR,v))
M is Element of VAR
H is Element of VAR
i is Element of VAR
v is Element of VAR
a is non empty set
K28(VAR,a) is set
K27(K28(VAR,a)) is set
m4 is Element of a
f is Element of a
p is Element of a
a is Element of a
r is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (M,m4)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (M,m4)) / (H,f)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (M,m4)) / (H,f)) / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (H,f)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (H,f)) / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (H,f)) / (i,p)) / (v,a)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (i,p)) / (v,a)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (i,p)) / (v,a)) / (M,m4)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (v,a)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (v,a)) / (H,f)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (v,a)) / (H,f)) / (i,p)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r / (M,m4)) / (i,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (M,m4)) / (i,p)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (M,m4)) / (i,p)) / (v,a)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r / (H,f)) / (i,p)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r / (H,f)) / (i,p)) / (M,m4)) / (v,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
M is Element of VAR
H is Element of VAR
i is Element of VAR
v is Element of VAR
a is non empty set
K28(VAR,a) is set
K27(K28(VAR,a)) is set
m4 is Element of a
f is Element of a
p is Element of a
a is Element of a
r is Element of a
r2 is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r2 / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (M,m4)) / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (M,m4)) / (H,f)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
r2 / (H,f) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (H,f)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (M,m4)) / (H,f)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (M,m4)) / (H,f)) / (i,a)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (H,f)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (i,a)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (M,m4)) / (H,f)) / (i,a)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((((r2 / (M,m4)) / (H,f)) / (i,a)) / (v,r)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (i,a)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (H,f)) / (i,a)) / (v,r)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(r2 / (H,f)) / (M,m4) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (M,m4)) / (M,p) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (M,m4)) / (H,f)) / (M,p)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((r2 / (H,f)) / (M,p)) / (i,a) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
((((r2 / (M,m4)) / (H,f)) / (i,a)) / (M,p)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
(((r2 / (H,f)) / (i,a)) / (M,p)) / (v,r) is Relation-like VAR -defined a -valued Function-like non empty V14( VAR ) V30( VAR ,a) Element of K27(K28(VAR,a))
M is Element of VAR
H is non empty set
K28(VAR,H) is set
K27(K28(VAR,H)) is set
i is Element of H

Free v is Element of K27(VAR)
a is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a / (M,i) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
a . M is Element of H
a / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))

(a / (M,i)) / (M,(a . M)) is Relation-like VAR -defined H -valued Function-like non empty V14( VAR ) V30( VAR ,H) Element of K27(K28(VAR,H))
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set

Free H is Element of K27(VAR)

All ((x. 4),(H <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
i is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,i) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
v is Element of M
(def_func' (H,i)) . v is Element of M
i / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a is Element of M
(i / ((x. 3),v)) / ((x. 4),a) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(i / ((x. 3),v)) . (x. 3) is Element of M
m4 is Element of VAR
((i / ((x. 3),v)) / ((x. 4),a)) . m4 is Element of M
i . m4 is Element of M
(i / ((x. 3),v)) . m4 is Element of M
((i / ((x. 3),v)) / ((x. 4),a)) . (x. 3) is Element of M
((i / ((x. 3),v)) / ((x. 4),a)) . (x. 4) is Element of M
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set

Free H is Element of K27(VAR)

All ((x. 4),(H <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(H <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func (H,M) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
i is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (H,i) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
v is Element of M
(def_func' (H,i)) . v is set
(def_func (H,M)) . v is set
(def_func' (H,i)) . v is Element of M
i / ((x. 3),v) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(i / ((x. 3),v)) / ((x. 4),((def_func' (H,i)) . v)) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
((i / ((x. 3),v)) / ((x. 4),((def_func' (H,i)) . v))) . (x. 3) is Element of M
(i / ((x. 3),v)) . (x. 3) is Element of M
((i / ((x. 3),v)) / ((x. 4),((def_func' (H,i)) . v))) . (x. 4) is Element of M
(def_func (H,M)) . v is Element of M
M is Element of VAR
H is Element of VAR
i is non empty set
K28(VAR,i) is set
K27(K28(VAR,i)) is set

variables_in v is non empty finite Element of K27(VAR)

a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
a / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
m4 is Element of VAR
f is Element of VAR

variables_in (m4 '=' f) is non empty finite Element of K27(VAR)
(m4 '=' f) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )

variables_in (m4 'in' f) is non empty finite Element of K27(VAR)
(m4 'in' f) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
p . M is Element of i
p / (H,(p . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a is Element of VAR
r is Element of VAR
(p / (H,(p . M))) . f is Element of i
p . r is Element of i
(p / (H,(p . M))) . m4 is Element of i
p . a is Element of i

p is Element of VAR
a is Element of VAR
r is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
r . M is Element of i
r / (H,(r . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(r / (H,(r . M))) . m4 is Element of i
r . p is Element of i
(r / (H,(r . M))) . f is Element of i
r . a is Element of i

variables_in m4 is non empty finite Element of K27(VAR)

variables_in f is non empty finite Element of K27(VAR)

variables_in (m4 '&' f) is non empty finite Element of K27(VAR)
(m4 '&' f) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
() \/ () is finite Element of K27(VAR)
p is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
p . M is Element of i
p / (H,(p . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(m4 / (H,M)) '&' (f / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
(m4 / (H,M)) '&' (f / (H,M)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )

variables_in m4 is non empty finite Element of K27(VAR)

f is Element of VAR

variables_in (All (f,m4)) is non empty finite Element of K27(VAR)
(All (f,m4)) / (H,M) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
p is Element of VAR
{f} is finite set
() \/ {f} is finite set
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
a / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
Free m4 is Element of K27(VAR)
All (p,(m4 / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
a / (M,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) . M is Element of i
(a / (M,r)) / (H,((a / (M,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) / (H,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (H,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,r)) / (M,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))

(a / (H,r)) . M is Element of i
((a / (H,r)) / (M,r)) / (M,((a / (H,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,r)) / (M,((a / (H,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))

r is Element of i
a / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (f,r)) . M is Element of i
(a / (f,r)) / (H,((a / (f,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . M))) / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
Free (All (f,m4)) is Element of K27(VAR)

All (M,(All (H,m4))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
a / (M,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) / (H,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,r)) . M is Element of i
All (M,(m4 / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
r is Element of i
(a / (H,(a . M))) / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (f,r) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (f,r)) / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (f,r)) . M is Element of i
(a / (f,r)) / (H,((a / (f,r)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
All (f,(m4 / (H,M))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )

variables_in m4 is non empty finite Element of K27(VAR)

variables_in ('not' m4) is non empty finite Element of K27(VAR)

f is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
f . M is Element of i
f / (H,(f . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))

M is Element of VAR
H is Element of VAR
i is non empty set
K28(VAR,i) is set
K27(K28(VAR,i)) is set

variables_in v is non empty finite Element of K27(VAR)

a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . H is Element of i
a / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) . M is Element of i
(a / (M,(a . H))) / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . H))) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
M is Element of VAR
H is Element of VAR
i is non empty set
K28(VAR,i) is set
K27(K28(VAR,i)) is set

Free v is Element of K27(VAR)

All ((x. 4),(v <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(v <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(v <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in v is non empty finite Element of K27(VAR)

Free (v / (H,M)) is Element of K27(VAR)
(v / (H,M)) <=> ((x. 4) '=' ()) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 4),((v / (H,M)) <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),((v / (H,M)) <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),((v / (H,M)) <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . H is Element of i
a / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
def_func' (v,a) is Relation-like i -defined i -valued Function-like non empty V14(i) V30(i,i) Element of K27(K28(i,i))
K28(i,i) is set
K27(K28(i,i)) is set
def_func' ((v / (H,M)),(a / (M,(a . H)))) is Relation-like i -defined i -valued Function-like non empty V14(i) V30(i,i) Element of K27(K28(i,i))
variables_in (v / (H,M)) is non empty finite Element of K27(VAR)
{M} is finite set
{H} is finite set
(Free v) \ {H} is Element of K27(VAR)
((Free v) \ {H}) \/ {M} is set
p is Element of i
a / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a is Element of i
(a / ((x. 3),p)) / ((),a) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / (M,(a . H))) / ((x. 3),p)) / ((),a) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
r2 is Element of i
((a / ((x. 3),p)) / ((),a)) / ((x. 4),r2) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(((a / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) . (x. 4) is Element of i
(((a / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) . () is Element of i
((a / ((x. 3),p)) / ((),a)) . () is Element of i
(((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) / ((x. 4),r2) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) . () is Element of i
(((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) . () is Element of i
((((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) . (x. 4) is Element of i
(((a / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) . M is Element of i
((((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) / (H,(((((a / (M,(a . H))) / ((x. 3),p)) / ((),a)) / ((x. 4),r2)) . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
p is Element of i
(def_func' (v,a)) . p is set
(def_func' ((v / (H,M)),(a / (M,(a . H))))) . p is set
(def_func' (v,a)) . p is Element of i
a / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) / ((x. 3),p) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) . H is Element of i
(((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) / (M,((((a / (M,(a . H))) / ((x. 3),p)) / ((x. 4),((def_func' (v,a)) . p))) . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(def_func' ((v / (H,M)),(a / (M,(a . H))))) . p is Element of i
M is Element of VAR
H is Element of VAR
i is non empty set

variables_in v is non empty finite Element of K27(VAR)

K28(VAR,i) is set
K27(K28(VAR,i)) is set
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . H is Element of i
a / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) . M is Element of i
(a / (M,(a . H))) / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
((a / (M,(a . H))) / (H,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (M,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (H,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . H))) / (M,(a . H)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
((a / (H,(a . H))) / (M,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
(a / (H,(a . H))) / (M,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
K28(VAR,i) is set
K27(K28(VAR,i)) is set
a is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
a . M is Element of i
a / (H,(a . M)) is Relation-like VAR -defined i -valued Function-like non empty V14( VAR ) V30( VAR ,i) Element of K27(K28(VAR,i))
M is non empty set
K28(VAR,M) is set
K27(K28(VAR,M)) is set
H is ext-real V18() V19() V20() V21() V25() V26() Element of NAT

Free i is Element of K27(VAR)

All ((x. 4),(i <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(i <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(i <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
v is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (i,v) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
K28(M,M) is set
K27(K28(M,M)) is set
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
a + 1 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT

Free m4 is Element of K27(VAR)

All ((x. 4),(m4 <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(m4 <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(m4 <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (m4,f) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
variables_in m4 is non empty finite Element of K27(VAR)
p is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
5 is non empty ext-real positive non negative V18() V19() V20() V21() V25() V26() Element of NAT
a is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. a is Element of VAR

variables_in r is non empty finite Element of K27(VAR)
Free r is Element of K27(VAR)

All ((x. 4),(r <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(r <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(r <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
f . () is Element of M
f / ((x. a),(f . ())) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (r,(f / ((x. a),(f . ())))) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
r2 is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. r2 is Element of VAR
x. a is Element of VAR

variables_in p is non empty finite Element of K27(VAR)
Free p is Element of K27(VAR)
a is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))

All ((x. 4),(p <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(p <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(p <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
def_func' (p,a) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
All ((x. 4),(x. a),p) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
variables_in (All ((x. 4),(x. a),p)) is non empty finite Element of K27(VAR)
r is ext-real V18() V19() V20() V21() V25() V26() Element of NAT
x. r is Element of VAR
p / ((x. a),(x. r)) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )

variables_in r2 is non empty finite Element of K27(VAR)
Free r2 is Element of K27(VAR)

All ((x. 4),(r2 <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),(r2 <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(r2 <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like finite V41() V42() ZF-formula-like M7( NAT )
a . (x. a) is Element of M
a / ((x. r),(a . (x. a))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
r is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
def_func' (r2,r) is Relation-like M -defined M -valued Function-like non empty V14(M) V30(M,M) Element of K27(K28(M,M))
{(x. 4),(x. a)} is finite set
() \/ {(x. 4),(x. a)} is finite set
r . (x. r) is Element of M
r / ((x. a),(r . (x. r))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
a / ((x. a),(r . (x. r))) is Relation-like VAR -defined M -valued Function-like non empty V14( VAR ) V30( VAR ,M) Element of K27(K28(VAR,M))
(a / ((x. a),(r . (x. r)))) / ((x. r),(a . (x. a))) is Relation-like VAR -defined M -valued Function-like non empty