:: TRANSLAC semantic presentation

begin

definition
let AS be ( ( V54() AffinSpace-like ) ( V49() V54() AffinSpace-like ) AffinSpace) ;
attr AS is Fanoian means :: TRANSLAC:def 1
 for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) holds
LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ;
end;

theorem :: TRANSLAC:1
for AS being ( ( V54() AffinSpace-like ) ( V49() V54() AffinSpace-like ) AffinSpace) st ex a, b, c being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st
( LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) holds
for p, q being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ex r being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st
( LIN p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) <> r : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) <> r : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) ;

theorem :: TRANSLAC:2
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is Fanoian & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st
( LIN b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) ;

theorem :: TRANSLAC:3
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for a, x, y being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) )
for f being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & not LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) ,x : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) // x : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) ,y : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) = f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) ;

theorem :: TRANSLAC:4
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) holds
( AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is translational iff for a, a9, b, c, b9, c9 being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) ;

theorem :: TRANSLAC:5
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for a being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ex f being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st
( f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) ;

theorem :: TRANSLAC:6
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for a, b, p, q being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st ( for p, q, r being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & not r : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) holds
r : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) = q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ;

theorem :: TRANSLAC:7
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for a, b being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) st AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is translational holds
ex f being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st
( f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) ;

theorem :: TRANSLAC:8
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) st ( for a, b being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ex f being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st
( f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ) ) holds
AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is translational ;

theorem :: TRANSLAC:9
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for a being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) )
for f, g being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & not LIN a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) ,g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . a : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) holds
f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) = g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: TRANSLAC:10
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for f, g being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is translational & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation holds
f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) = g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: TRANSLAC:11
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for p being ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) )
for f, g being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) // p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) holds
p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) . p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) // p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) ,(f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) . p : ( ( ) ( ) Element of ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) )) ;

theorem :: TRANSLAC:12
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for f being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is Fanoian & AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is translational & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation holds
ex g being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st
( g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) = f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) ) ;

theorem :: TRANSLAC:13
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for f being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is Fanoian & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) = id the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) : ( ( V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) ) ( V1() V4( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) V5( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) V6() V8() V9() V13() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) holds
f : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) = id the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) : ( ( V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) ) ( V1() V4( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) V5( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) V6() V8() V9() V13() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) ;

theorem :: TRANSLAC:14
for AFP being ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane)
for f1, f2, g being ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) st AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is translational & AFP : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) is Fanoian & f1 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & f2 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) is translation & g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) = f1 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * f1 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) & g : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) = f2 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) * f2 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) M2(K19(K20( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) , the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) )) holds
f1 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) = f2 : ( ( V14() quasi_total bijective ) ( V1() V14() V15() V19() V22( the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) quasi_total onto bijective ) Permutation of the carrier of b1 : ( ( V54() AffinSpace-like 2-dimensional ) ( V49() V54() AffinSpace-like 2-dimensional ) AffinPlane) : ( ( ) ( V19() V20() ) set ) ) ;