let N be invertible Matrix of 3,F_Real; :: thesis: for NR being Matrix of 3,REAL
for P, Q being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3)
for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
(homography N) . P = Q
let NR be Matrix of 3,REAL; :: thesis: for P, Q being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3)
for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
(homography N) . P = Q
let P, Q be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u, v being non zero Element of (TOP-REAL 3)
for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
(homography N) . P = Q
let u, v be non zero Element of (TOP-REAL 3); :: thesis: for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
(homography N) . P = Q
let vfr, ufr be FinSequence of REAL ; :: thesis: ( P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr implies (homography N) . P = Q )
assume A1: ( P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr ) ; :: thesis: (homography N) . P = Q
consider u1, v1 being Element of (TOP-REAL 3), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that
A2: ( P = Dir u1 & not u1 is zero & u1 = u1f & p1 = N * u1f & v1 = M2F p1 & not v1 is zero & (homography N) . P = Dir v1 ) by ANPROJ_8:def 4;
reconsider u1fr = u1f as FinSequence of REAL ;
u1 in TOP-REAL 3 ;
then u1 in REAL 3 by EUCLID:22;
then A3: len u1fr = 3 by A2, EUCLID_8:50;
then A4: v1 = NR * u1fr by A1, A2, Th30;
are_Prop u,u1 by A1, A2, ANPROJ_1:22;
then consider a being Real such that
A5: a <> 0 and
A6: u = a * u1 by ANPROJ_1:1;
A7: width NR = 3 by MATRIX_0:23;
A8: ( width NR = len u1fr & len u1fr > 0 ) by A3, MATRIX_0:23;
A9: len NR = 3 by MATRIX_0:24;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then ( width NR = len ufr & len ufr > 0 ) by A7, A1, EUCLID_8:50;
then ( len (NR * ufr) = 3 & len (NR * u1fr) = 3 ) by A9, A3, MATRIX_0:23, MATRIXR1:61;
then ( NR * ufr is Element of REAL 3 & NR * u1fr is Element of REAL 3 ) by EUCLID_8:2;
then reconsider w1 = NR * ufr, w2 = NR * u1fr as Element of (TOP-REAL 3) by EUCLID:22;
w1 = a * w2 by A8, A1, A2, A6, MATRIXR1:59;
then are_Prop w1,w2 by A5, ANPROJ_1:1;
hence (homography N) . P = Q by A1, A2, A4, ANPROJ_1:22; :: thesis: verum