defpred S1[ object , object ] means ex x being Point of (ProjectiveSpace (TOP-REAL 3)) st
( x = $1 & ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & $2 = Dir v ) );
A1:
for x being object st x in the carrier of (ProjectiveSpace (TOP-REAL 3)) holds
ex y being object st
( y in the carrier of (ProjectiveSpace (TOP-REAL 3)) & S1[x,y] )
proof
let x be
object ;
( x in the carrier of (ProjectiveSpace (TOP-REAL 3)) implies ex y being object st
( y in the carrier of (ProjectiveSpace (TOP-REAL 3)) & S1[x,y] ) )
assume
x in the
carrier of
(ProjectiveSpace (TOP-REAL 3))
;
ex y being object st
( y in the carrier of (ProjectiveSpace (TOP-REAL 3)) & S1[x,y] )
then reconsider x1 =
x as
Element of
(ProjectiveSpace (TOP-REAL 3)) ;
consider u being
Element of
(TOP-REAL 3) such that A2:
not
u is
zero
and A3:
x1 = Dir u
by ANPROJ_1:26;
reconsider uf =
u as
FinSequence of
F_Real by EUCLID:24;
A4:
N * (<*uf*> @) is 3,1
-size
by FINSEQ_3:153, Th74;
A5:
N * (<*uf*> @) is
Matrix of 3,1,
F_Real
by FINSEQ_3:153, Th74;
N * (<*uf*> @) is
FinSequence of 1
-tuples_on REAL
by A4, Th79;
then reconsider p =
N * uf as
FinSequence of 1
-tuples_on REAL by LAPLACE:def 9;
A6:
the
carrier of
(ProjectiveSpace (TOP-REAL 3)) = ProjectivePoints (TOP-REAL 3)
by ANPROJ_1:23;
len p =
len (N * (<*uf*> @))
by LAPLACE:def 9
.=
3
by A5, MATRIX_0:23
;
then reconsider v =
M2F p as
Element of
(TOP-REAL 3) by Th66;
set y =
Dir v;
A7:
Dir v is
Element of
ProjectivePoints (TOP-REAL 3)
by A2, Th82, ANPROJ_1:21;
hence
ex
y being
object st
(
y in the
carrier of
(ProjectiveSpace (TOP-REAL 3)) &
S1[
x,
y] )
by A7, A6;
verum
end;
ex f being Function of the carrier of (ProjectiveSpace (TOP-REAL 3)), the carrier of (ProjectiveSpace (TOP-REAL 3)) st
for x being object st x in the carrier of (ProjectiveSpace (TOP-REAL 3)) holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
then consider f being Function of the carrier of (ProjectiveSpace (TOP-REAL 3)), the carrier of (ProjectiveSpace (TOP-REAL 3)) such that
A8:
for x being object st x in the carrier of (ProjectiveSpace (TOP-REAL 3)) holds
S1[x,f . x]
;
for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & f . x = Dir v )
hence
ex b1 being Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) st
for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b1 . x = Dir v )
; verum