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:]
F1() is non empty set
[:F1(),F1():] is set
bool [:F1(),F1():] is set
AFP is Element of F1()
AFP is V1() V4(F1()) V5(F1()) Function-like non empty V22(F1()) quasi_total Element of bool [:F1(),F1():]
K is set
p is Element of F1()
AFP . p is Element of F1()
rng AFP is Element of bool F1()
bool F1() is set
K is set
p is set
AFP . K is set
AFP . p is set
K is V1() V4(F1()) V5(F1()) Function-like one-to-one non empty V22(F1()) quasi_total onto bijective Element of bool [:F1(),F1():]
p is Element of F1()
K . p is Element of F1()
f is Element of F1()
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 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
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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a 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
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
x is Element of the carrier of AFP
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
K is Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . 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
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
a is Element of the carrier of AFP
b is Element of the carrier of AFP
b is Element of the carrier of AFP
A is Element of the carrier of AFP
a is Element of the carrier of AFP
b 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
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:]
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
(id the carrier of AFP) . 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
x is Element of the carrier of AFP
K . x 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
K . x is Element of the carrier of AFP
x is Element of the carrier of AFP
K . x is Element of 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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
b is Element of the carrier of AFP
K . b is Element of the carrier of AFP
A 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x . 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
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:]
K is Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
f . a is Element of the carrier of AFP
f . x is Element of the carrier of AFP
(id the carrier of AFP) . 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
K is Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x " 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,f,(x ")) 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,f,(x ")) . p is Element of the carrier of AFP
(x ") . (x . p) is Element of the carrier of AFP
( the carrier of AFP,f,(x ")) . K is Element of the carrier of AFP
(x ") . (x . K) is Element of the carrier of AFP
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:]
a is Element of the carrier of AFP
f . a is Element of the carrier of AFP
(x ") . (f . a) is Element of the carrier of AFP
( the carrier of AFP,f,(x ")) . a is Element of the carrier of AFP
x . 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
[: 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:]
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:]
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
x is Element of the carrier of AFP
K . x is Element of 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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
b is Element of the carrier of AFP
K . b 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . 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 Element of 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:]
p . K is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
a is Element of the carrier of AFP
p . a is Element of the carrier of AFP
f . a is Element of the carrier of AFP
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:]
b is Element of the carrier of AFP
p . b is Element of the carrier of AFP
f . b is Element of the carrier of AFP
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:]
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
K . p is Element of the carrier of AFP
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:]
p is Element of the carrier of AFP
K . 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:]
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:]
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:]
f is Element of the carrier of AFP
( the carrier of AFP,p,K) . f is Element of the carrier of AFP
p . f is Element of the carrier of AFP
K . (p . f) is Element of 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:]
(K ") . f is Element of the carrier of AFP
( the carrier of AFP,(K "),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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x is Element of the carrier of AFP
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:]
f . 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
K is Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
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:]
x is Element of the carrier of AFP
a is Element of the carrier of AFP
f . x is Element of the carrier of AFP
b 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
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:]
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
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
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:]
p is Element of the carrier of AFP
K . 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x . 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x . f is Element of the carrier of AFP
a is Element of the carrier of AFP
x . 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 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
a 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 . K is Element of the carrier of AFP
a . p is Element of the carrier of AFP
a . x is Element of the carrier of AFP
a . 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 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
a 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 . K is Element of the carrier of AFP
a . p is Element of the carrier of AFP
a . x is Element of the carrier of AFP
a . f is Element of the carrier of AFP
b is Element of the carrier of AFP
A is Element of the carrier of AFP
a . b is Element of the carrier of AFP
a . 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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x is Element of the carrier of AFP
f . x is Element of the carrier of AFP
a is Element of the carrier of AFP
f . 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 Element of 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:]
p . K is Element of 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
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
a is Element of the carrier of AFP
p . a is Element of the carrier of AFP
b is Element of the carrier of AFP
p . b 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
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
f is Element of the carrier of AFP
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
f is Element of the carrier of AFP
K . f is Element of the carrier of AFP
p is Element of the carrier of AFP
K . p is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
Lambda AFP is non empty strict AffinStruct
AFP is non empty non trivial AffinSpace-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 AffinSpace-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
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
AFP is non empty non trivial AffinSpace-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 AffinSpace-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 AffinSpace-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 AffinSpace-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
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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
f is Element of the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
b is Element of the carrier of AFP
b is Element of the carrier of AFP
A is Element of the carrier of AFP
a is Element of the carrier of AFP
b is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
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:]
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
(id the carrier of AFP) . 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
x is Element of the carrier of AFP
K . x 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
K . x is Element of the carrier of AFP
x is Element of the carrier of AFP
K . x is Element of 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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
b is Element of the carrier of AFP
K . b is Element of the carrier of AFP
A is Element of the carrier of AFP
K . A is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 Element of the carrier of AFP
p is Element of the carrier of AFP
f is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x . f is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
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:]
K is Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
f . a is Element of the carrier of AFP
f . x is Element of the carrier of AFP
(id the carrier of AFP) . x is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x " 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,f,(x ")) 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,f,(x ")) . p is Element of the carrier of AFP
(x ") . (x . p) is Element of the carrier of AFP
( the carrier of AFP,f,(x ")) . K is Element of the carrier of AFP
(x ") . (x . K) is Element of the carrier of AFP
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:]
a is Element of the carrier of AFP
f . a is Element of the carrier of AFP
(x ") . (f . a) is Element of the carrier of AFP
( the carrier of AFP,f,(x ")) . a is Element of the carrier of AFP
x . a is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
f is Element of the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 AffinSpace-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 AffinSpace-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:]
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:]
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
x is Element of the carrier of AFP
K . x is Element of 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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
b is Element of the carrier of AFP
K . b is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 Element of the carrier of AFP
p is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 Element of 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:]
p . K is Element of the carrier of AFP
f 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 . K is Element of the carrier of AFP
a is Element of the carrier of AFP
p . a is Element of the carrier of AFP
f . a is Element of the carrier of AFP
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:]
b is Element of the carrier of AFP
p . b is Element of the carrier of AFP
f . b is Element of the carrier of AFP
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:]
AFP is non empty non trivial AffinSpace-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
K . p is Element of the carrier of AFP
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:]
p is Element of the carrier of AFP
K . p is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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:]
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:]
f is Element of the carrier of AFP
( the carrier of AFP,p,K) . f is Element of the carrier of AFP
p . f is Element of the carrier of AFP
K . (p . f) is Element of 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:]
(K ") . f is Element of the carrier of AFP
( the carrier of AFP,(K "),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 AffinSpace-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 AffinSpace-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:]
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
K . f is Element of the carrier of AFP
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
[p,f] is set
[x,a] is set
[[p,f],[x,a]] is set
[(K . p),(K . f)] is set
[(K . x),(K . a)] is set
[[(K . p),(K . f)],[(K . x),(K . a)]] is set
[(K . p),(K . f)] is set
[(K . x),(K . a)] is set
[[(K . p),(K . f)],[(K . x),(K . a)]] is set
[p,f] is set
[x,a] is set
[[p,f],[x,a]] is set
p is Element of 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
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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
[x,a] is set
[[p,f],[x,a]] is set
K . a is Element of the carrier of AFP
[(K . x),(K . a)] is set
[[(K . p),(K . f)],[(K . x),(K . a)]] is set
AFP is non empty non trivial AffinSpace-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 Element of the carrier of AFP
p is Element of the carrier of AFP
f is Element of the carrier of AFP
x 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:]
x . K is Element of the carrier of AFP
x . p is Element of the carrier of AFP
x . f is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
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:]
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 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 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 non trivial AffinSpace-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
bool the carrier of AFP is set
K is Element of 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:]
p . K is Element of the carrier of AFP
f is Element of bool the carrier of AFP
p .: f is Element of bool the carrier of AFP
dom p is Element of bool the carrier of AFP
AFP is non empty non trivial AffinSpace-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
bool the carrier of AFP is set
K is Element of 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:]
f is Element of bool the carrier of AFP
p .: f is Element of bool the carrier of AFP
dom p is Element of bool the carrier of AFP
x is set
p . x is set
x is Element of the carrier of AFP
p . x is Element of the carrier of AFP
dom p is Element of bool the carrier of AFP
AFP is non empty non trivial AffinSpace-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
bool 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 bool the carrier of AFP
K .: p is Element of bool the carrier of AFP
f is Element of bool the carrier of AFP
K .: f is Element of bool the carrier of AFP
x is set
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
A is Element of the carrier of AFP
K . A is Element of the carrier of AFP
x is set
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
A is Element of the carrier of AFP
K . A is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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 Element of the carrier of AFP
p is Element of the carrier of AFP
Line (K,p) is Element of bool the carrier of AFP
bool the carrier of AFP is set
f 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 .: (Line (K,p)) is Element of bool the carrier of AFP
f . K is Element of the carrier of AFP
f . p is Element of the carrier of AFP
Line ((f . K),(f . p)) is Element of bool the carrier of AFP
x is set
a is Element of the carrier of AFP
b is Element of the carrier of AFP
f . b is Element of the carrier of AFP
x is set
a is Element of the carrier of AFP
b is Element of the carrier of AFP
f . b is Element of the carrier of AFP
AFP is non empty non trivial AffinSpace-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
bool 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 bool the carrier of AFP
K .: p is Element of bool the carrier of AFP
f is Element of the carrier of AFP
x is Element of the carrier of AFP
Line (f,x) is Element of bool the carrier of AFP
K . x is Element of the carrier of AFP
K . f is Element of the carrier of AFP
Line ((K . f),(K . x)) is Element of bool the carrier of AFP
AFP is non empty non trivial AffinSpace-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
bool 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 bool the carrier of AFP
K .: p is Element of bool the carrier of AFP
f is Element of bool the carrier of AFP
K .: f is Element of bool the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
b is Element of the carrier of AFP
A is Element of the carrier of AFP
Line (x,a) is Element of bool the carrier of AFP
Line (b,A) is Element of bool the carrier of AFP
K . x is Element of the carrier of AFP
K . a is Element of the carrier of AFP
K . b is Element of the carrier of AFP
K . A is Element of the carrier of AFP
Line ((K . x),(K . a)) is Element of bool the carrier of AFP
Line ((K . b),(K . A)) is Element of bool the carrier of AFP
AFP is non empty non trivial AffinSpace-like 2-dimensional 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
bool 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
K . p is Element of the carrier of AFP
f is Element of the carrier of AFP
Line (p,f) is Element of bool the carrier of AFP
K .: (Line (p,f)) is Element of bool the carrier of AFP
K . f is Element of the carrier of AFP
Line ((K . p),(K . f)) is Element of bool the carrier of AFP
p is Element of bool the carrier of AFP
K .: p is Element of bool the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
Line (x,a) is Element of bool the carrier of AFP
b is Element of the carrier of AFP
K . b is Element of the carrier of AFP
A is Element of the carrier of AFP
K . A is Element of the carrier of AFP
Line (A,b) is Element of bool the carrier of AFP
K .: (Line (A,b)) is Element of bool the carrier of AFP
p is Element of bool the carrier of AFP
K .: p is Element of bool the carrier of AFP
f is Element of bool the carrier of AFP
K .: f is Element of bool the carrier of AFP
b is Element of the carrier of AFP
K . b is Element of 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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
Line (x,a) is Element of bool the carrier of AFP
Line (p,f) is Element of bool the carrier of AFP
K .: (Line (p,f)) is Element of bool the carrier of AFP
K .: (Line (x,a)) is Element of bool the carrier of AFP
Line ((K . p),(K . f)) is Element of bool the carrier of AFP
Line ((K . x),(K . a)) is Element of bool the carrier of AFP
p is Element of bool the carrier of AFP
K .: p is Element of bool the carrier of AFP
f is Element of bool the carrier of AFP
K .: f is Element of bool the carrier of AFP
x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
b is Element of the carrier of AFP
K . b is Element of 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
x is Element of the carrier of AFP
K . x is Element of the carrier of AFP
a is Element of the carrier of AFP
K . a is Element of the carrier of AFP
Line (x,a) is Element of bool the carrier of AFP
Line (p,f) is Element of bool the carrier of AFP
K .: (Line (p,f)) is Element of bool the carrier of AFP
K .: (Line (x,a)) is Element of bool the carrier of AFP
AFP is non empty non trivial AffinSpace-like 2-dimensional AffinStruct
the carrier of AFP is non empty non trivial set
bool the carrier of AFP is set
[: the carrier of AFP, the carrier of AFP:] is set
bool [: the carrier of AFP, the carrier of AFP:] is 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:]
K is Element of bool the carrier of AFP
p is Element of the carrier of AFP
f 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 . p is Element of the carrier of AFP
x is Element of the carrier of AFP
f . x is Element of the carrier of AFP
a is Element of the carrier of AFP
b is Element of the carrier of AFP
Line (p,a) is Element of bool the carrier of AFP
f .: (Line (p,a)) is Element of bool the carrier of AFP
f . a is Element of the carrier of AFP
Line ((f . p),(f . a)) is Element of bool the carrier of AFP
C is Element of bool the carrier of AFP
f .: C is Element of bool the carrier of AFP
c is Element of the carrier of AFP
f . c is Element of the carrier of AFP
Line (p,b) is Element of bool the carrier of AFP
f .: (Line (p,b)) is Element of bool the carrier of AFP
f . b is Element of the carrier of AFP
Line ((f . p),(f . b)) is Element of bool the carrier of AFP
D is Element of bool the carrier of AFP
f .: D is Element of bool the carrier of AFP
d is Element of the carrier of AFP
f . d is Element of the carrier of AFP
x is Element of the carrier of AFP
f . x is Element of the carrier of AFP
(id the carrier of AFP) . x is Element of the carrier of AFP