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_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple 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_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple 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_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple 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_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple 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;
cross-ratio (P,Q,R,S) <> 0 by A3, A4, Th31;
then reconsider cr = cross-ratio-tuple x as non zero Complex by A1, Th36;
( pi_1243 x = <*P,Q,S,R*> & P,Q,S,R are_collinear & P,Q,S,R are_mutually_distinct ) by A4, A1, A3, ZFMISC_1:def 6;
then A5: cross-ratio-tuple (pi_1324 (pi_1243 x)) = 1 - (cross-ratio-tuple (pi_1243 x)) by Th41
.= 1 - (1 / cr) by A1, A3, A4, Th40
.= (cr / cr) - (1 / cr) by XCMPLX_1:60
.= (cr - 1) / cr ;
hence cross-ratio-tuple (pi_1423 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) ; :: thesis: ( cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) )
( pi_1423 x = <*P,S,Q,R*> & P,S,Q,R are_collinear ) by A1, A3;
then ( cross-ratio-tuple (pi_3412 (pi_1423 x)) = cross-ratio-tuple (pi_1423 x) & cross-ratio-tuple (pi_2143 (pi_1423 x)) = cross-ratio-tuple (pi_1423 x) & cross-ratio-tuple (pi_4321 (pi_1423 x)) = cross-ratio-tuple (pi_1423 x) ) by A4, Th37, Th38;
hence ( cross-ratio-tuple (pi_2314 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_4132 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) & cross-ratio-tuple (pi_3241 x) = ((cross-ratio-tuple x) - 1) / (cross-ratio-tuple x) ) by A5; :: thesis: verum