let N be invertible Matrix of 3,F_Real; :: thesis: for a, b, c being non zero Element of F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds
( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )
let a, b, c be non zero Element of F_Real; :: thesis: ( N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> implies ( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 ) )
assume A1: N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> ; :: thesis: ( (homography N) . Dir100 = Dir100 & (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )
thus (homography N) . Dir100 = Dir100 :: thesis: ( (homography N) . Dir010 = Dir010 & (homography N) . Dir001 = Dir001 )

proof

consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that
A2: Dir100 = Dir u and
A3: not u is zero and
A4: u = uf and
A5: p = N * uf and
A6: v = M2F p and
A7: not v is zero and
A8: (homography N) . Dir100 = Dir v by ANPROJ_8:def 4;
not |[1,0,0]| is zero by EUCLID_8:def 1, Th13;
then are_Prop u,|[1,0,0]| by A2, A3, ANPROJ_1:22;
then consider d being Real such that
d <> 0 and
A9: u = d * |[1,0,0]| by ANPROJ_1:1;
A10: u = |[(d * 1),(d * 0),(d * 0)]| by A9, EUCLID_5:8
.= |[d,0,0]| ;
then ( u `1 = d & u `2 = 0 & u `3 = 0 ) by EUCLID_5:2;
then A11: ( uf . 1 = d & uf . 2 = 0 & uf . 3 = 0 ) by A4, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A12: <*uf*> @ = <*<*d*>,<*0*>,<*0*>*> by A11, A4, EUCLID_8:50, ANPROJ_8:77;
then reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by ANPROJ_8:4;
reconsider z = 0 as Element of F_Real ;
reconsider d = d as Element of F_Real by XREAL_0:def 1;
A13: p = N * Mu by A5, LAPLACE:def 9
.= <*<*(((a * d) + (z * z)) + (z * z))*>,<*(((z * d) + (b * z)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by A1, A12, Th08
.= <*<*(a * d)*>,<*0*>,<*0*>*> ;
v = |[(a * d),0,0]|

proof

A14: ( <*(a * d)*> . 1 = a * d & <*0*> . 1 = 0 ) ;
A15: ( p . 1 = <*(a * d)*> & p . 2 = <*0*> & p . 3 = <*0*> ) by A13;
len p = 3 by A13, FINSEQ_1:45;
hence v = |[(a * d),0,0]| by A14, A15, A6, ANPROJ_8:def 2; :: thesis: verum

end;

then A16: v = |[(a * d),(a * 0),(a * 0)]|
.= a * u by A10, EUCLID_5:8 ;
not a is zero ;
then are_Prop v,u by A16, ANPROJ_1:1;
hence (homography N) . Dir100 = Dir100 by A2, A3, A7, A8, ANPROJ_1:22; :: thesis: verum

end;

thus (homography N) . Dir010 = Dir010 :: thesis: (homography N) . Dir001 = Dir001

proof

consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that
A17: Dir010 = Dir u and
A18: not u is zero and
A19: u = uf and
A20: p = N * uf and
A21: v = M2F p and
A22: not v is zero and
A23: (homography N) . Dir010 = Dir v by ANPROJ_8:def 4;
not |[0,1,0]| is zero by EUCLID_8:def 2, Th13;
then are_Prop u,|[0,1,0]| by A17, A18, ANPROJ_1:22;
then consider d being Real such that
d <> 0 and
A24: u = d * |[0,1,0]| by ANPROJ_1:1;
A25: u = |[(d * 0),(d * 1),(d * 0)]| by A24, EUCLID_5:8
.= |[0,d,0]| ;
then ( u `1 = 0 & u `2 = d & u `3 = 0 ) by EUCLID_5:2;
then A26: ( uf . 1 = 0 & uf . 2 = d & uf . 3 = 0 ) by A19, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A27: <*uf*> @ = <*<*0*>,<*d*>,<*0*>*> by A26, A19, EUCLID_8:50, ANPROJ_8:77;
reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A27, ANPROJ_8:4;
reconsider z = 0 as Element of F_Real ;
reconsider d = d as Element of F_Real by XREAL_0:def 1;
A28: p = N * Mu by A20, LAPLACE:def 9
.= <*<*(((a * z) + (z * d)) + (z * z))*>,<*(((z * z) + (b * d)) + (z * z))*>,<*(((z * d) + (z * z)) + (c * z))*>*> by A1, A27, Th08
.= <*<*0*>,<*(b * d)*>,<*0*>*> ;
v = |[0,(b * d),0]|

proof

A29: ( <*0*> . 1 = 0 & <*(b * d)*> . 1 = b * d ) ;
A30: ( p . 1 = <*0*> & p . 2 = <*(b * d)*> & p . 3 = <*0*> ) by A28;
len p = 3 by A28, FINSEQ_1:45;
hence v = |[0,(b * d),0]| by A29, A30, A21, ANPROJ_8:def 2; :: thesis: verum

end;

then A31: v = |[(b * 0),(b * d),(b * 0)]|
.= b * u by A25, EUCLID_5:8 ;
not b is zero ;
then are_Prop v,u by A31, ANPROJ_1:1;
hence (homography N) . Dir010 = Dir010 by A17, A18, A22, A23, ANPROJ_1:22; :: thesis: verum

end;

thus (homography N) . Dir001 = Dir001 :: thesis: verum

proof

consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that
A31BIS: Dir001 = Dir u and
A32: not u is zero and
A33: u = uf and
A34: p = N * uf and
A35: v = M2F p and
A36: not v is zero and
A37: (homography N) . Dir001 = Dir v by ANPROJ_8:def 4;
not |[0,0,1]| is zero by EUCLID_8:def 3, Th13;
then are_Prop u,|[0,0,1]| by A31BIS, A32, ANPROJ_1:22;
then consider d being Real such that
d <> 0 and
A38: u = d * |[0,0,1]| by ANPROJ_1:1;
A39: u = |[(d * 0),(d * 0),(d * 1)]| by A38, EUCLID_5:8
.= |[0,0,d]| ;
then ( u `1 = 0 & u `2 = 0 & u `3 = d ) by EUCLID_5:2;
then A40: ( uf . 1 = 0 & uf . 2 = 0 & uf . 3 = d ) by A33, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A41: <*uf*> @ = <*<*0*>,<*0*>,<*d*>*> by A40, A33, EUCLID_8:50, ANPROJ_8:77;
reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A41, ANPROJ_8:4;
reconsider z = 0 as Element of F_Real ;
reconsider d = d as Element of F_Real by XREAL_0:def 1;
A42: p = N * Mu by A34, LAPLACE:def 9
.= <*<*(((a * z) + (z * z)) + (z * d))*>,<*(((z * z) + (b * z)) + (z * d))*>,<*(((z * z) + (z * z)) + (c * d))*>*> by A1, A41, Th08
.= <*<*0*>,<*0*>,<*(c * d)*>*> ;
v = |[0,0,(c * d)]|

proof

A43: ( <*(c * d)*> . 1 = c * d & <*0*> . 1 = 0 ) ;
A44: ( p . 3 = <*(c * d)*> & p . 2 = <*0*> & p . 1 = <*0*> ) by A42;
len p = 3 by A42, FINSEQ_1:45;
hence v = |[0,0,(c * d)]| by A43, A44, A35, ANPROJ_8:def 2; :: thesis: verum

end;

then A45: v = |[(c * 0),(c * 0),(c * d)]|
.= c * u by A39, EUCLID_5:8 ;
not c is zero ;
then are_Prop v,u by A45, ANPROJ_1:1;
hence (homography N) . Dir001 = Dir001 by A31BIS, A32, A36, A37, ANPROJ_1:22; :: thesis: verum

end;