defpred S₁[ object , object ] means ex x being LINE of (IncProjSp_of real_projective_plane) st
( $1 = x & $2 = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } );
A1: for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds
ex y being object st
( y in the Lines of (IncProjSp_of real_projective_plane) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the Lines of (IncProjSp_of real_projective_plane) implies ex y being object st
( y in the Lines of (IncProjSp_of real_projective_plane) & S₁[x,y] ) )
assume x in the Lines of (IncProjSp_of real_projective_plane) ; :: thesis: ex y being object st
( y in the Lines of (IncProjSp_of real_projective_plane) & S₁[x,y] )
then reconsider x9 = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;
set y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ;
consider p, q being Point of real_projective_plane such that
A2: p <> q and
A3: x9 = Line (p,q) by COLLSP:def 7, INCPROJ:4;
reconsider p9 = (homography N) . p, q9 = (homography N) . q as Point of real_projective_plane by FUNCT_2:5;
A4: { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (p9,q9)

proof

A5: { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } c= Line (p9,q9)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } or x in Line (p9,q9) )
assume x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ; :: thesis: x in Line (p9,q9)
then consider Px being POINT of (IncProjSp_of real_projective_plane) such that
A6: x = (homography N) . Px and
A7: Px on x9 ;
reconsider Px = Px as Point of real_projective_plane by INCPROJ:3;
x9 is LINE of real_projective_plane by INCPROJ:4;
then A8: Px in x9 by A7, INCPROJ:5;
reconsider p1 = p, q1 = q, r1 = Px, p2 = p9, q2 = q9 as Point of (ProjectiveSpace (TOP-REAL 3)) ;
(homography N) . p1,(homography N) . q1,(homography N) . r1 are_collinear by A8, A3, COLLSP:11, ANPROJ_8:102;
hence x in Line (p9,q9) by A6, COLLSP:11; :: thesis: verum

end;

Line (p9,q9) c= { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (p9,q9) or x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } )
assume x in Line (p9,q9) ; :: thesis: x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }
then x in { p where p is Element of real_projective_plane : p9,q9,p are_collinear } by COLLSP:def 5;
then consider x99 being Element of real_projective_plane such that
A9: x = x99 and
A10: p9,q9,x99 are_collinear ;
reconsider p1 = p, q1 = q, r1 = x99, p2 = p9, q2 = q9 as Point of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider r2 = (homography (N ~)) . r1 as Point of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider r3 = r2 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
A11: r1 = (homography N) . r2 by ANPROJ_9:15;
A12: x9 is LINE of real_projective_plane by INCPROJ:4;
r2 in x9 by A3, A10, A11, ANPROJ_8:102, COLLSP:11;
then r3 on x9 by A12, INCPROJ:5;
hence x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } by A11, A9; :: thesis: verum

end;

hence { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (p9,q9) by A5; :: thesis: verum

end;

reconsider y9 = Line (p9,q9) as LINE of real_projective_plane by A2, ANPROJ_9:16, COLLSP:def 7;
reconsider y = y9 as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
y is Element of the Lines of (IncProjSp_of real_projective_plane) ;
then reconsider y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } as Element of the Lines of (IncProjSp_of real_projective_plane) by A4;
take y ; :: thesis: ( y in the Lines of (IncProjSp_of real_projective_plane) & S₁[x,y] )
thus ( y in the Lines of (IncProjSp_of real_projective_plane) & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) such that
A13: for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
for x being LINE of (IncProjSp_of real_projective_plane) holds f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }

proof

let x be LINE of (IncProjSp_of real_projective_plane); :: thesis: f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }
S₁[x,f . x] by A13;
hence f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ; :: thesis: verum

end;

hence ex b₁ being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) st
for x being LINE of (IncProjSp_of real_projective_plane) holds b₁ . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ; :: thesis: verum