let P1, P2, P3, P4 be Point of (); :: 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
( () . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 & () . 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
( () . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 & () . 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 ;
set Q1 = () . P1;
set Q2 = () . P2;
set Q3 = () . P3;
set Q4 = () . P4;
( not (homography N1) . P1,() . P2,() . P3 are_collinear & not () . P1,() . P2,() . P4 are_collinear & not () . P1,() . P3,() . P4 are_collinear & not () . P2,() . P3,() . P4 are_collinear ) by ;
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
() . (() . 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: ( () . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 & () . 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 = () . (() . P1) by
.= (homography (N2 * N1)) . P1 by Th14 ; :: thesis: ( Dir010 = (homography (N2 * N1)) . P2 & Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )
thus Dir010 = () . (() . P2) by
.= (homography (N2 * N1)) . P2 by Th14 ; :: thesis: ( Dir001 = (homography (N2 * N1)) . P3 & Dir111 = (homography (N2 * N1)) . P4 )
thus Dir001 = () . (() . P3) by
.= (homography (N2 * N1)) . P3 by Th14 ; :: thesis: Dir111 = (homography (N2 * N1)) . P4
thus Dir111 = () . (() . P4) by A8
.= (homography (N2 * N1)) . P4 by Th14 ; :: thesis: verum
end;
hence ( (homography N) . P1 = Dir100 & () . P2 = Dir010 & () . P3 = Dir001 & () . P4 = Dir111 ) ; :: thesis: verum