defpred S₁[ 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)) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (ProjectiveSpace (TOP-REAL 3)) implies ex y being object st
( y in the carrier of (ProjectiveSpace (TOP-REAL 3)) & S₁[x,y] ) )
assume x in the carrier of (ProjectiveSpace (TOP-REAL 3)) ; :: thesis: ex y being object st
( y in the carrier of (ProjectiveSpace (TOP-REAL 3)) & S₁[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;

now :: thesis: ex x1 being Element of (ProjectiveSpace (TOP-REAL 3)) st
( x1 = x & 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
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v ) )

take x1 = x1; :: thesis: ( x1 = x & 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
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v ) )
thus x1 = x ; :: thesis: 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
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )

now :: thesis: 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
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )

take u = u; :: thesis: ex v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
take v = v; :: thesis: ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
take uf = uf; :: thesis: ex p being FinSequence of 1 -tuples_on REAL st
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
take p = p; :: thesis: ( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
thus x1 = Dir u by A3; :: thesis: ( not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
thus not u is zero by A2; :: thesis: ( u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
thus u = uf ; :: thesis: ( p = N * uf & v = M2F p & not v is zero & Dir v = Dir v )
thus p = N * uf ; :: thesis: ( v = M2F p & not v is zero & Dir v = Dir v )
thus v = M2F p ; :: thesis: ( not v is zero & Dir v = Dir v )
thus not v is zero by A2, Th82; :: thesis: Dir v = Dir v
thus Dir v = Dir v ; :: thesis: verum

end;

hence 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
( x1 = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & Dir v = Dir v ) ; :: thesis: verum

end;

hence ex y being object st
( y in the carrier of (ProjectiveSpace (TOP-REAL 3)) & S₁[x,y] ) by A7, A6; :: thesis: 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
S₁[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
S₁[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 )

proof

let x be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: 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 )
S₁[x,f . x] by A8;
hence 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 ) ; :: thesis: verum

end;

hence ex b₁ 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 & b₁ . x = Dir v ) ; :: thesis: verum