:: HOMOTHET semantic presentation

K82() is M2(K19(K78()))
K78() is set
K19(K78()) is set
K77() is set
K19(K77()) is set
K19(K82()) is set
K14() is set
1 is V11() set

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
Line (a,b) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
Line (a,f) is M2(K19( the carrier of AFP))
Line (a,B9) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
f is M2( the carrier of AFP)
a is M2(K19( the carrier of AFP))
b is M2(K19( the carrier of AFP))
K is M2(K19( the carrier of AFP))
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2(K19( the carrier of AFP))
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
a is M2(K19( the carrier of AFP))
b is M2( the carrier of AFP)
A is M2( the carrier of AFP)
y is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2(K19( the carrier of AFP))
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2(K19( the carrier of AFP))
Line (b,f) is M2(K19( the carrier of AFP))
Line (b,K) is M2(K19( the carrier of AFP))
C is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2(K19( the carrier of AFP))
b is M2(K19( the carrier of AFP))
K is M2(K19( the carrier of AFP))
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
Line (a,K) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
C9 is M2( the carrier of AFP)
Line (a,b) is M2(K19( the carrier of AFP))
Line (A,K) is M2(K19( the carrier of AFP))
x is M2(K19( the carrier of AFP))
N is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
y . a is M2( the carrier of AFP)
y . b is M2( the carrier of AFP)
y . B9 is M2( the carrier of AFP)
y . f is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
Line (a,b) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
Line (K,f) is M2(K19( the carrier of AFP))

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
Line (a,K) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
Line (a,B9) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
Line (a,b) is M2(K19( the carrier of AFP))

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
Line (a,A) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
Line (b,A) is M2(K19( the carrier of AFP))
y is M2(K19( the carrier of AFP))
p is M2( the carrier of AFP)
Line (a,b) is M2(K19( the carrier of AFP))
Line (A,f) is M2(K19( the carrier of AFP))
C is M2(K19( the carrier of AFP))
y is M2( the carrier of AFP)
A is M2( the carrier of AFP)
A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
p is M2( the carrier of AFP)
C9 is M2( the carrier of AFP)
C is M2( the carrier of AFP)
q is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
Line (a,p) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
Line (a,b) is M2(K19( the carrier of AFP))
Line (a,x) is M2(K19( the carrier of AFP))
Line (a,x) is M2(K19( the carrier of AFP))
C9 is M2( the carrier of AFP)
C is M2( the carrier of AFP)
C9 is M2( the carrier of AFP)
C is M2( the carrier of AFP)
C9 is M2( the carrier of AFP)
C is M2( the carrier of AFP)
C9 is M2( the carrier of AFP)
C is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
f is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
C9 is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
Line (a,b) is M2(K19( the carrier of AFP))
K19( the carrier of AFP) is set
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
Line (K,B9) is M2(K19( the carrier of AFP))

the carrier of AFP is V11() V12() set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
f . a is M2( the carrier of AFP)
f . b is M2( the carrier of AFP)
A is M2( the carrier of AFP)
f . A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
f . B9 is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
C9 is M2( the carrier of AFP)
C is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
f . b is M2( the carrier of AFP)
f . a is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set

the carrier of f is V11() V12() set
K20( the carrier of f, the carrier of f) is set
K19(K20( the carrier of f, the carrier of f)) is set

the carrier of AFP is V11() V12() set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
K19( the carrier of AFP) is set

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
id the carrier of AFP is V14( the carrier of AFP) M2(K19(K20( the carrier of AFP, the carrier of AFP)))
a is M2( the carrier of AFP)
b is M2(K19( the carrier of AFP))
K is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
K . a is M2( the carrier of AFP)
f is M2( the carrier of AFP)
K . f is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2(K19( the carrier of AFP))
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
p . A is M2( the carrier of AFP)
p . x is M2( the carrier of AFP)
p . a is M2( the carrier of AFP)
id the carrier of AFP is V14( the carrier of AFP) M2(K19(K20( the carrier of AFP, the carrier of AFP)))
p . f is M2( the carrier of AFP)
p . K is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2(K19( the carrier of AFP))
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
Line (A,b) is M2(K19( the carrier of AFP))
Line (A,a) is M2(K19( the carrier of AFP))
p is M2(K19( the carrier of AFP))
q is M2( the carrier of AFP)
C9 is M2(K19( the carrier of AFP))
C is M2(K19( the carrier of AFP))
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
y is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2(K19( the carrier of AFP))
q is M2(K19( the carrier of AFP))
Line (f,x) is M2(K19( the carrier of AFP))
Line (K,y) is M2(K19( the carrier of AFP))
Line (b,A) is M2(K19( the carrier of AFP))
Line (a,B9) is M2(K19( the carrier of AFP))
N is M2( the carrier of AFP)
z is M2( the carrier of AFP)
z is M2( the carrier of AFP)
N is M2( the carrier of AFP)
z is M2(K19( the carrier of AFP))
z is M2( the carrier of AFP)
N is M2( the carrier of AFP)
z is M2( the carrier of AFP)
z is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2(K19( the carrier of AFP))
Line (a,K) is M2(K19( the carrier of AFP))
C9 is M2( the carrier of AFP)
Line (a,b) is M2(K19( the carrier of AFP))
Line (K,B9) is M2(K19( the carrier of AFP))

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2(K19( the carrier of AFP))
C9 is M2(K19( the carrier of AFP))
Line (B9,p) is M2(K19( the carrier of AFP))

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2(K19( the carrier of AFP))
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
f is M2( the carrier of AFP)
f is M2( the carrier of AFP)
f is M2( the carrier of AFP)
A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
f . a is M2( the carrier of AFP)
A is M2( the carrier of AFP)
B9 is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
A is M2( the carrier of AFP)
f . A is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
A is M2(K19( the carrier of AFP))
f .: A is M2(K19( the carrier of AFP))
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
f . y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
f . y is M2( the carrier of AFP)
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
x is M2(K19( the carrier of AFP))
y is M2(K19( the carrier of AFP))
p is M2( the carrier of AFP)
q is M2( the carrier of AFP)
Line (q,b) is M2(K19( the carrier of AFP))
C is M2(K19( the carrier of AFP))
y is M2( the carrier of AFP)
x is M2(K19( the carrier of AFP))
N is M2( the carrier of AFP)
f . N is M2( the carrier of AFP)
f . p is M2( the carrier of AFP)
y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
f . x is M2( the carrier of AFP)
N is M2(K19( the carrier of AFP))
z is M2( the carrier of AFP)
x is M2( the carrier of AFP)
y is M2( the carrier of AFP)
f . y is M2( the carrier of AFP)
x is M2( the carrier of AFP)
f . x is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
A is M2( the carrier of AFP)
f . A is M2( the carrier of AFP)
A is M2( the carrier of AFP)
f . A is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
f is V6() quasi_total bijective M2(K19(K20( the carrier of AFP, the carrier of AFP)))
f . a is M2( the carrier of AFP)

the carrier of AFP is V11() V12() set
K19( the carrier of AFP) is set
a is M2( the carrier of AFP)
b is M2( the carrier of AFP)
K is M2(K19( the carrier of AFP))
K20( the carrier of AFP, the carrier of AFP) is set
K19(K20( the carrier of AFP, the carrier of AFP)) is set

the carrier of f is V11() V12() set
K19( the carrier of f) is set
K20( the carrier of f, the carrier of f) is set
K19(K20( the carrier of f, the carrier of f)) is set