let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not Dir100 , Dir010 ,P are_collinear & not Dir100 , Dir001 ,P are_collinear & not Dir010 , Dir001 ,P are_collinear implies ex a, b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111 )

assume that

A1: not Dir100 , Dir010 ,P are_collinear and

A2: not Dir100 , Dir001 ,P are_collinear and

A3: not Dir010 , Dir001 ,P are_collinear ; :: thesis: ex a, b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

consider a, b, c being non zero Element of F_Real such that

A4: P = Dir |[a,b,c]| by Th23, A1, A2, A3;

reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;

( not ia is zero & not ib is zero & not ic is zero ) by XCMPLX_1:50;

then reconsider ia = ia, ib = ib, ic = ic as non zero Element of F_Real ;

take ia ; :: thesis: ex b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

take ib ; :: thesis: ex c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

take ic ; :: thesis: for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir111

thus for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir111 by A4, Th24; :: thesis: verum

for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111 )

assume that

A1: not Dir100 , Dir010 ,P are_collinear and

A2: not Dir100 , Dir001 ,P are_collinear and

A3: not Dir010 , Dir001 ,P are_collinear ; :: thesis: ex a, b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

consider a, b, c being non zero Element of F_Real such that

A4: P = Dir |[a,b,c]| by Th23, A1, A2, A3;

reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;

( not ia is zero & not ib is zero & not ic is zero ) by XCMPLX_1:50;

then reconsider ia = ia, ib = ib, ic = ic as non zero Element of F_Real ;

take ia ; :: thesis: ex b, c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

take ib ; :: thesis: ex c being non zero Element of F_Real st

for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,c*>*> holds

(homography N) . P = Dir111

take ic ; :: thesis: for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir111

thus for N being invertible Matrix of 3,F_Real st N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds

(homography N) . P = Dir111 by A4, Th24; :: thesis: verum