:: TRANSGEO semantic presentation

K107() is Element of bool K103()

K103() is set

bool K103() is set

K102() is set

bool K102() is set

bool K107() is set

{} is Function-like functional empty set

1 is non empty set

AFP is set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p * K is V1() Function-like one-to-one set

p * K is V1() V4(AFP) V5(AFP) Function-like one-to-one V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is Element of AFP

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

rng p is Element of bool AFP

bool AFP is set

dom p is Element of bool AFP

f is set

p . f is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is Element of AFP

p is Element of AFP

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f . K is Element of AFP

f " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(f ") . p is Element of AFP

dom f is Element of bool AFP

bool AFP is set

rng f is Element of bool AFP

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,K,p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

F

[:F

bool [:F

AFP is Element of F

AFP is V1() V4(F

K is set

p is Element of F

AFP . p is Element of F

rng AFP is Element of bool F

bool F

K is set

p is set

AFP . K is set

AFP . p is set

K is V1() V4(F

p is Element of F

K . p is Element of F

f is Element of F

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

f is non empty set

[:f,f:] is set

bool [:f,f:] is set

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K is Element of AFP

(p ") . K is Element of AFP

p . ((p ") . K) is Element of AFP

a is V1() V4(f) V5(f) Function-like one-to-one non empty V22(f) quasi_total onto bijective Element of bool [:f,f:]

a " is V1() V4(f) V5(f) Function-like one-to-one non empty V22(f) quasi_total onto bijective Element of bool [:f,f:]

x is Element of f

a . x is Element of f

(a ") . (a . x) is Element of f

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(id AFP),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,(id AFP)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,(K ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,(AFP,K,(K "))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,f,K),(K ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,(AFP,K,(K "))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,(id AFP)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,(id AFP)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(p "),p),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,p,f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(p "),p),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(id AFP),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(id AFP),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,K),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,K),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,p,K),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,p,f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,K,f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,f),(AFP,K,f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,(id AFP)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,(id AFP)),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(AFP,p,(id AFP)),K),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,(AFP,p,(id AFP)),K),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,(f ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,(AFP,f,(f "))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,(AFP,f,(f "))),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(AFP,p,(AFP,f,(f "))),K),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,(AFP,p,(AFP,f,(f "))),K),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,f),(f ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(AFP,p,f),(f ")),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(AFP,(AFP,p,f),(f ")),K),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,(AFP,(AFP,p,f),(f ")),K),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,f),(AFP,(f "),K)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(AFP,p,f),(AFP,(f "),K)),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,(AFP,p,f),(AFP,(f "),K)),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(f "),K),f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,p,f),(AFP,(AFP,(f "),K),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,p,f),(AFP,(AFP,(f "),K),f))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(f "),(AFP,p,f)),(AFP,(AFP,(f "),K),f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(K "),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(K "),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,(K "),p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,K,p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(p ") " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,((AFP,K,p) "),((p ") ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(K ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(p "),(K ")),((p ") ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(p "),(K ")),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,(AFP,f,p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,p) " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,(AFP,f,p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,((AFP,f,p) "),(AFP,K,(AFP,f,p))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,K,f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,K,f),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,K,f),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,(AFP,K,f),p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(f ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,(p "),(f ")),(AFP,K,(AFP,f,p))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,K,(AFP,f,p))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,(f "),(AFP,K,(AFP,f,p)))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(AFP,K,f),p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,(AFP,K,f),p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,(f "),(AFP,(AFP,K,f),p))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(id AFP),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(id AFP),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(K "),(AFP,(id AFP),K)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(K "),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,(id AFP)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(id AFP) " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,(id AFP)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,((id AFP) "),(AFP,K,(id AFP))) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,((id AFP) "),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(id AFP),K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

K is Element of AFP

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p . K is Element of AFP

f is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,f) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(f "),(AFP,p,f)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f . K is Element of AFP

(AFP,p,f) . (f . K) is Element of AFP

(f ") . (f . K) is Element of AFP

(AFP,f,(f ")) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,f,(f ")) . K is Element of AFP

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(id AFP) . K is Element of AFP

(AFP,p,f) . K is Element of AFP

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

AFP is non empty set

[:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

bool [:AFP,AFP:] is set

K is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

p is Element of AFP

(id AFP) . p is Element of AFP

f is Element of AFP

[p,f] is set

(id AFP) . f is Element of AFP

[((id AFP) . p),((id AFP) . f)] is set

[[p,f],[((id AFP) . p),((id AFP) . f)]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

f is Element of AFP

(K ") . f is Element of AFP

x is Element of AFP

[f,x] is set

(K ") . x is Element of AFP

[((K ") . f),((K ") . x)] is set

[[f,x],[((K ") . f),((K ") . x)]] is set

K . ((K ") . f) is Element of AFP

K . ((K ") . x) is Element of AFP

[(K . ((K ") . f)),(K . ((K ") . x))] is set

[[((K ") . f),((K ") . x)],[(K . ((K ") . f)),(K . ((K ") . x))]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

x is Element of AFP

(AFP,p,K) . x is Element of AFP

a is Element of AFP

[x,a] is set

(AFP,p,K) . a is Element of AFP

[((AFP,p,K) . x),((AFP,p,K) . a)] is set

[[x,a],[((AFP,p,K) . x),((AFP,p,K) . a)]] is set

p . x is Element of AFP

K . (p . x) is Element of AFP

p . a is Element of AFP

K . (p . a) is Element of AFP

[(p . x),(p . a)] is set

[[(p . x),(p . a)],[((AFP,p,K) . x),((AFP,p,K) . a)]] is set

[[x,a],[(p . x),(p . a)]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,p,K) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

x is Element of AFP

(AFP,p,K) . x is Element of AFP

a is Element of AFP

[x,a] is set

(AFP,p,K) . a is Element of AFP

[((AFP,p,K) . x),((AFP,p,K) . a)] is set

[[x,a],[((AFP,p,K) . x),((AFP,p,K) . a)]] is set

p . x is Element of AFP

K . (p . x) is Element of AFP

p . a is Element of AFP

K . (p . a) is Element of AFP

[(p . x),(p . a)] is set

[[(p . x),(p . a)],[((AFP,p,K) . x),((AFP,p,K) . a)]] is set

[[x,a],[(p . x),(p . a)]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

AFP is non empty set

[:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

id AFP is V1() V4(AFP) V5(AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

bool [:AFP,AFP:] is set

K is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

p is Element of AFP

(id AFP) . p is Element of AFP

f is Element of AFP

[p,f] is set

(id AFP) . f is Element of AFP

[((id AFP) . p),((id AFP) . f)] is set

x is Element of AFP

(id AFP) . x is Element of AFP

a is Element of AFP

[x,a] is set

[[p,f],[x,a]] is set

(id AFP) . a is Element of AFP

[((id AFP) . x),((id AFP) . a)] is set

[[((id AFP) . p),((id AFP) . f)],[((id AFP) . x),((id AFP) . a)]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

K " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

f is Element of AFP

(K ") . f is Element of AFP

x is Element of AFP

[f,x] is set

(K ") . x is Element of AFP

[((K ") . f),((K ") . x)] is set

a is Element of AFP

(K ") . a is Element of AFP

b is Element of AFP

[a,b] is set

[[f,x],[a,b]] is set

(K ") . b is Element of AFP

[((K ") . a),((K ") . b)] is set

[[((K ") . f),((K ") . x)],[((K ") . a),((K ") . b)]] is set

K . ((K ") . a) is Element of AFP

K . ((K ") . b) is Element of AFP

K . ((K ") . f) is Element of AFP

K . ((K ") . x) is Element of AFP

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

x is Element of AFP

(AFP,K,p) . x is Element of AFP

a is Element of AFP

[x,a] is set

(AFP,K,p) . a is Element of AFP

[((AFP,K,p) . x),((AFP,K,p) . a)] is set

b is Element of AFP

(AFP,K,p) . b is Element of AFP

A is Element of AFP

[b,A] is set

[[x,a],[b,A]] is set

(AFP,K,p) . A is Element of AFP

[((AFP,K,p) . b),((AFP,K,p) . A)] is set

[[((AFP,K,p) . x),((AFP,K,p) . a)],[((AFP,K,p) . b),((AFP,K,p) . A)]] is set

K . x is Element of AFP

p . (K . x) is Element of AFP

K . a is Element of AFP

p . (K . a) is Element of AFP

K . b is Element of AFP

p . (K . b) is Element of AFP

K . A is Element of AFP

p . (K . A) is Element of AFP

[(K . x),(K . a)] is set

[(K . b),(K . A)] is set

[[(K . x),(K . a)],[(K . b),(K . A)]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

f is Element of AFP

K . f is Element of AFP

x is Element of AFP

[f,x] is set

K . x is Element of AFP

[(K . f),(K . x)] is set

a is Element of AFP

K . a is Element of AFP

b is Element of AFP

[a,b] is set

[[f,x],[a,b]] is set

K . b is Element of AFP

[(K . a),(K . b)] is set

[[(K . f),(K . x)],[(K . a),(K . b)]] is set

[[a,b],[(K . a),(K . b)]] is set

[[(K . a),(K . b)],[a,b]] is set

[[f,x],[(K . f),(K . x)]] is set

[[f,x],[(K . a),(K . b)]] is set

[[(K . f),(K . x)],[f,x]] is set

[[(K . f),(K . x)],[a,b]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

f is Element of AFP

[f,f] is set

x is Element of AFP

a is Element of AFP

[x,a] is set

[[x,a],[f,f]] is set

[[f,f],[x,a]] is set

f is Element of AFP

K . f is Element of AFP

x is Element of AFP

[f,x] is set

K . x is Element of AFP

[(K . f),(K . x)] is set

a is Element of AFP

K . a is Element of AFP

b is Element of AFP

[a,b] is set

[[f,x],[a,b]] is set

K . b is Element of AFP

[(K . a),(K . b)] is set

[[(K . f),(K . x)],[(K . a),(K . b)]] is set

[[f,x],[(K . f),(K . x)]] is set

[[a,b],[(K . a),(K . b)]] is set

[[(K . a),(K . b)],[a,b]] is set

[[f,x],[(K . a),(K . b)]] is set

[[(K . f),(K . x)],[f,x]] is set

[[(K . f),(K . x)],[a,b]] is set

AFP is non empty set

[:AFP,AFP:] is set

bool [:AFP,AFP:] is set

[:[:AFP,AFP:],[:AFP,AFP:]:] is set

bool [:[:AFP,AFP:],[:AFP,AFP:]:] is set

K is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

p " is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,K,p) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

(AFP,(p "),(AFP,K,p)) is V1() V4(AFP) V5(AFP) Function-like one-to-one non empty V22(AFP) quasi_total onto bijective Element of bool [:AFP,AFP:]

f is V1() V4([:AFP,AFP:]) V5([:AFP,AFP:]) Element of bool [:[:AFP,AFP:],[:AFP,AFP:]:]

x is Element of AFP

(AFP,K,p) . x is Element of AFP

a is Element of AFP

[x,a] is set

(AFP,K,p) . a is Element of AFP

[((AFP,K,p) . x),((AFP,K,p) . a)] is set

[[x,a],[((AFP,K,p) . x),((AFP,K,p) . a)]] is set

(p ") . x is Element of AFP

(p ") . a is Element of AFP

[((p ") . x),((p ") . a)] is set

K . ((p ") . x) is Element of AFP

K . ((p ") . a) is Element of AFP

[(K . ((p ") . x)),(K . ((p ") . a))] is set

[[((p ") . x),((p ") . a)],[(K . ((p ") . x)),(K . ((p ") . a))]] is set

p . ((p ") . x) is Element of AFP

p . ((p ") . a) is Element of AFP

p . (K . ((p ") . x)) is Element of AFP

p . (K . ((p ") . a)) is Element of AFP

[(p . (K . ((p ") . x))),(p . (K . ((p ") . a)))] is set

[[x,a],[(p . (K . ((p ") . x))),(p . (K . ((p ") . a)))]] is set

(AFP,K,p) . ((p ") . x) is Element of AFP

[((AFP,K,p) . ((p ") . x)),(p . (K . ((p ") . a)))] is set

[[x,a],[((AFP,K,p) . ((p ") . x)),(p . (K . ((p ") . a)))]] is set

(AFP,K,p) . ((p ") . a) is Element of AFP

[((AFP,K,p) . ((p ") . x)),((AFP,K,p) . ((p ") . a))] is set

[[x,a],[((AFP,K,p) . ((p ") . x)),((AFP,K,p) . ((p ") . a))]] is set

(AFP,(p "),(AFP,K,p)) . x is Element of AFP

[((AFP,(p "),(AFP,K,p)) . x),((AFP,K,p) . ((p ") . a))] is set

[[x,a],[((AFP,(p "),(AFP,K,p)) . x),((AFP,K,p) . ((p ") . a))]] is set

AFP is non empty AffinStruct

the carrier of AFP is non empty set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

AFP is non empty AffinStruct

the carrier of AFP is non empty set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

p is Element of the carrier of AFP

K . p is Element of the carrier of AFP

f is Element of the carrier of AFP

[p,f] is set

K . f is Element of the carrier of AFP

[(K . p),(K . f)] is set

[[p,f],[(K . p),(K . f)]] is set

p is Element of the carrier of AFP

f is Element of the carrier of AFP

[p,f] is set

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

[(K . p),(K . f)] is set

[[p,f],[(K . p),(K . f)]] is set

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

x is Element of the carrier of AFP

a is Element of the carrier of AFP

K . x is Element of the carrier of AFP

K . a is Element of the carrier of AFP

the non empty non trivial strict OAffinSpace-like AffinStruct is non empty non trivial strict OAffinSpace-like AffinStruct

the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct is non empty non trivial set

K is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

p is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

f is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

x is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

a is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

b is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

K is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

p is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

a is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

b is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

f is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

x is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

A is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

C is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

c is Element of the carrier of the non empty non trivial strict OAffinSpace-like AffinStruct

AFP is non empty () AffinStruct

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

the carrier of AFP is non empty set

[: the carrier of AFP, the carrier of AFP:] is set

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

K is set

[K,K] is set

p is Element of the carrier of AFP

f is Element of the carrier of AFP

[p,f] is set

AFP is non empty () AffinStruct

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

the carrier of AFP is non empty set

[: the carrier of AFP, the carrier of AFP:] is set

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

K is set

p is set

[K,p] is set

[p,K] is set

f is Element of the carrier of AFP

x is Element of the carrier of AFP

[f,x] is set

a is Element of the carrier of AFP

b is Element of the carrier of AFP

[a,b] is set

AFP is non empty () AffinStruct

the carrier of AFP is non empty set

id the carrier of AFP is V1() V4( the carrier of AFP) V5( the carrier of AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

AFP is non empty () AffinStruct

the carrier of AFP is non empty set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

K " is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

AFP is non empty () AffinStruct

the carrier of AFP is non empty set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

( the carrier of AFP,p,K) is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

a is Element of the carrier of AFP

b is Element of the carrier of AFP

[a,b] is set

f is Element of the carrier of AFP

x is Element of the carrier of AFP

[f,x] is set

[[a,b],[f,x]] is set

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

A is Element of the carrier of AFP

C is Element of the carrier of AFP

[A,C] is set

[[f,x],[A,C]] is set

[[a,b],[A,C]] is set

f is Element of the carrier of AFP

x is Element of the carrier of AFP

a is Element of the carrier of AFP

[f,f] is set

[x,a] is set

[[f,f],[x,a]] is set

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

K is Element of the carrier of AFP

p is Element of the carrier of AFP

a is Element of the carrier of AFP

b is Element of the carrier of AFP

f is Element of the carrier of AFP

x is Element of the carrier of AFP

K is Element of the carrier of AFP

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K is Element of the carrier of AFP

p is Element of the carrier of AFP

f is Element of the carrier of AFP

x is Element of the carrier of AFP

K is Element of the carrier of AFP

p is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

x is Element of the carrier of AFP

a is Element of the carrier of AFP

K . x is Element of the carrier of AFP

K . a is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

id the carrier of AFP is V1() V4( the carrier of AFP) V5( the carrier of AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

K " is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

( the carrier of AFP,p,K) is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

K " is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is Element of the carrier of AFP

(K ") . p is Element of the carrier of AFP

f is Element of the carrier of AFP

(K ") . f is Element of the carrier of AFP

K . ((K ") . p) is Element of the carrier of AFP

K . ((K ") . f) is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

( the carrier of AFP,p,K) is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

( the carrier of AFP,K,p) is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

f is Element of the carrier of AFP

( the carrier of AFP,p,K) . f is Element of the carrier of AFP

x is Element of the carrier of AFP

( the carrier of AFP,p,K) . x is Element of the carrier of AFP

p . f is Element of the carrier of AFP

p . x is Element of the carrier of AFP

K . (p . f) is Element of the carrier of AFP

K . (p . x) is Element of the carrier of AFP

f is Element of the carrier of AFP

( the carrier of AFP,K,p) . f is Element of the carrier of AFP

x is Element of the carrier of AFP

( the carrier of AFP,K,p) . x is Element of the carrier of AFP

K . f is Element of the carrier of AFP

K . x is Element of the carrier of AFP

p . (K . f) is Element of the carrier of AFP

p . (K . x) is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

[p,f] is set

[(K . p),(K . f)] is set

[[p,f],[(K . p),(K . f)]] is set

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

lambda the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

p is Element of the carrier of AFP

f is Element of the carrier of AFP

[p,f] is set

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

[(K . p),(K . f)] is set

[[p,f],[(K . p),(K . f)]] is set

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

x is Element of the carrier of AFP

a is Element of the carrier of AFP

K . x is Element of the carrier of AFP

K . a is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is Element of the carrier of AFP

f is Element of the carrier of AFP

K . p is Element of the carrier of AFP

K . f is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

Lambda AFP is non empty strict AffinStruct

the carrier of (Lambda AFP) is non empty set

[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):] is set

bool [: the carrier of (Lambda AFP), the carrier of (Lambda AFP):] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

lambda the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

AffinStruct(# the carrier of AFP,(lambda the CONGR of AFP) #) is strict AffinStruct

p is V1() V4( the carrier of (Lambda AFP)) V5( the carrier of (Lambda AFP)) Function-like one-to-one non empty V22( the carrier of (Lambda AFP)) quasi_total onto bijective Element of bool [: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]

AFP is non empty non trivial OAffinSpace-like AffinStruct

Lambda AFP is non empty strict AffinStruct

the carrier of (Lambda AFP) is non empty set

[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):] is set

bool [: the carrier of (Lambda AFP), the carrier of (Lambda AFP):] is set

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of (Lambda AFP)) V5( the carrier of (Lambda AFP)) Function-like one-to-one non empty V22( the carrier of (Lambda AFP)) quasi_total onto bijective Element of bool [: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]

the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

[:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:] is set

lambda the CONGR of AFP is V1() V4([: the carrier of AFP, the carrier of AFP:]) V5([: the carrier of AFP, the carrier of AFP:]) Element of bool [:[: the carrier of AFP, the carrier of AFP:],[: the carrier of AFP, the carrier of AFP:]:]

AffinStruct(# the carrier of AFP,(lambda the CONGR of AFP) #) is strict AffinStruct

the CONGR of (Lambda AFP) is V1() V4([: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]) V5([: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]) Element of bool [:[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):],[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]:]

[:[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):],[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]:] is set

bool [:[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):],[: the carrier of (Lambda AFP), the carrier of (Lambda AFP):]:] is set

p is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

id the carrier of AFP is V1() V4( the carrier of AFP) V5( the carrier of AFP) reflexive symmetric antisymmetric transitive Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is Element of the carrier of AFP

(id the carrier of AFP) . K is Element of the carrier of AFP

p is Element of the carrier of AFP

(id the carrier of AFP) . p is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

K " is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is Element of the carrier of AFP

(K ") . p is Element of the carrier of AFP

f is Element of the carrier of AFP

(K ") . f is Element of the carrier of AFP

K . ((K ") . p) is Element of the carrier of AFP

K . ((K ") . f) is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non empty non trivial set

[: the carrier of AFP, the carrier of AFP:] is set

bool [: the carrier of AFP, the carrier of AFP:] is set

K is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

p is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

( the carrier of AFP,p,K) is V1() V4( the carrier of AFP) V5( the carrier of AFP) Function-like one-to-one non empty V22( the carrier of AFP) quasi_total onto bijective Element of bool [: the carrier of AFP, the carrier of AFP:]

f is Element of the carrier of AFP

p . f is Element of the carrier of AFP

x is Element of the carrier of AFP

p . x is Element of the carrier of AFP

( the carrier of AFP,p,K) . f is Element of the carrier of AFP

K . (p . f) is Element of the carrier of AFP

( the carrier of AFP,p,K) . x is Element of the carrier of AFP

K . (p . x) is Element of the carrier of AFP

AFP is non empty non trivial OAffinSpace-like AffinStruct

the carrier of AFP is non