let P1, P2, P3, P4 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear implies ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 ) )
assume that
A1: not P1,P2,P3 are_collinear and
A2: not P1,P2,P4 are_collinear and
A3: not P1,P3,P4 are_collinear and
A4: not P2,P3,P4 are_collinear ; :: thesis: ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )
consider N1 being invertible Matrix of 3,F_Real such that
A5: (homography N1) . P1 = Dir100 and
A6: (homography N1) . P2 = Dir010 and
A7: (homography N1) . P3 = Dir001 by A1, Th20;
set Q1 = (homography N1) . P1;
set Q2 = (homography N1) . P2;
set Q3 = (homography N1) . P3;
set Q4 = (homography N1) . P4;
( not (homography N1) . P1,(homography N1) . P2,(homography N1) . P3 are_collinear & not (homography N1) . P1,(homography N1) . P2,(homography N1) . P4 are_collinear & not (homography N1) . P1,(homography N1) . P3,(homography N1) . P4 are_collinear & not (homography N1) . P2,(homography N1) . P3,(homography N1) . P4 are_collinear ) by A1, A2, A3, A4, ANPROJ_8:102;
then consider a, b, c being non zero Element of F_Real such that
A8: for N2 being invertible Matrix of 3,F_Real st N2 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
(homography N2) . ((homography N1) . P4) = Dir111 by A5, A6, A7, Th25;
reconsider N2 = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> as invertible Matrix of 3,F_Real by Th10;
reconsider N = N2 * N1 as invertible Matrix of 3,F_Real ;
take N ; :: thesis: ( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 )

now :: thesis: ( Dir100 = (homography (N2 * N1)) . P1 & Dir010 = (homography (N2 * N1)) . P2 & Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )

thus Dir100 = (homography N2) . ((homography N1) . P1) by A5, Th21
.= (homography (N2 * N1)) . P1 by Th14 ; :: thesis: ( Dir010 = (homography (N2 * N1)) . P2 & Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )
thus Dir010 = (homography N2) . ((homography N1) . P2) by A6, Th21
.= (homography (N2 * N1)) . P2 by Th14 ; :: thesis: ( Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )
thus Dir001 = (homography N2) . ((homography N1) . P3) by A7, Th21
.= (homography (N2 * N1)) . P3 by Th14 ; :: thesis: Dir111 = (homography (N2 * N1)) . P4
thus Dir111 = (homography N2) . ((homography N1) . P4) by A8
.= (homography (N2 * N1)) . P4 by Th14 ; :: thesis: verum

end;

hence ( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 & (homography N) . P4 = Dir111 ) ; :: thesis: verum