let V be RealLinearSpace; :: thesis: for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple (pi_1324 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_2413 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_3142 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_4231 x) = 1 - (cross-ratio-tuple x) )
let P, Q, R, S be Element of V; :: thesis: for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple (pi_1324 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_2413 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_3142 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_4231 x) = 1 - (cross-ratio-tuple x) )
let x be Tuple of 4, the carrier of V; :: thesis: ( x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear implies ( cross-ratio-tuple (pi_1324 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_2413 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_3142 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_4231 x) = 1 - (cross-ratio-tuple x) ) )
assume that
A1: x = <*P,Q,R,S*> and
A2: P,Q,R,S are_mutually_distinct and
A3: P,Q,R,S are_collinear ; :: thesis: ( cross-ratio-tuple (pi_1324 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_2413 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_3142 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_4231 x) = 1 - (cross-ratio-tuple x) )
A4: ( P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q ) by A2, ZFMISC_1:def 6;
A6: ( pi_1324 x = <*P,R,Q,S*> & P,R,Q,S are_collinear ) by A3, A1;
now :: thesis: ( cross-ratio-tuple (pi_1324 x) = cross-ratio (P,R,Q,S) & cross-ratio-tuple x = cross-ratio (P,Q,R,S) & cross-ratio-tuple (pi_2413 x) = cross-ratio-tuple (pi_1324 x) & cross-ratio-tuple (pi_3142 x) = cross-ratio-tuple (pi_1324 x) & cross-ratio-tuple (pi_4231 x) = cross-ratio-tuple (pi_1324 x) )
( x . 1 = P & x . 2 = Q & x . 3 = R & x . 4 = S & (pi_1324 x) . 1 = P & (pi_1324 x) . 2 = R & (pi_1324 x) . 3 = Q & (pi_1324 x) . 4 = S ) by A1;
hence ( cross-ratio-tuple (pi_1324 x) = cross-ratio (P,R,Q,S) & cross-ratio-tuple x = cross-ratio (P,Q,R,S) ) by Def03; :: thesis: ( cross-ratio-tuple (pi_2413 x) = cross-ratio-tuple (pi_1324 x) & cross-ratio-tuple (pi_3142 x) = cross-ratio-tuple (pi_1324 x) & cross-ratio-tuple (pi_4231 x) = cross-ratio-tuple (pi_1324 x) )
thus cross-ratio-tuple (pi_2413 x) = cross-ratio-tuple (pi_3412 (pi_1324 x))
.= cross-ratio-tuple (pi_1324 x) by A6, A4, Th37 ; :: thesis: ( cross-ratio-tuple (pi_3142 x) = cross-ratio-tuple (pi_1324 x) & cross-ratio-tuple (pi_4231 x) = cross-ratio-tuple (pi_1324 x) )
thus cross-ratio-tuple (pi_3142 x) = cross-ratio-tuple (pi_2143 (pi_1324 x))
.= cross-ratio-tuple (pi_1324 x) by A4, Th38, A6 ; :: thesis: cross-ratio-tuple (pi_4231 x) = cross-ratio-tuple (pi_1324 x)
thus cross-ratio-tuple (pi_4231 x) = cross-ratio-tuple (pi_4321 (pi_1324 x))
.= cross-ratio-tuple (pi_1324 x) by A4, Th38, A6 ; :: thesis: verum
end;
hence ( cross-ratio-tuple (pi_1324 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_2413 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_3142 x) = 1 - (cross-ratio-tuple x) & cross-ratio-tuple (pi_4231 x) = 1 - (cross-ratio-tuple x) ) by A2, A3, Th35; :: thesis: verum