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_collinear & P <> R & P <> S & Q <> R & Q <> S holds
( cross-ratio-tuple x = cross-ratio-tuple (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 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_collinear & P <> R & P <> S & Q <> R & Q <> S holds
( cross-ratio-tuple x = cross-ratio-tuple (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 x) )
let x be Tuple of 4, the carrier of V; :: thesis: ( x = <*P,Q,R,S*> & P,Q,R,S are_collinear & P <> R & P <> S & Q <> R & Q <> S implies ( cross-ratio-tuple x = cross-ratio-tuple (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 x) ) )
assume that
A1: x = <*P,Q,R,S*> and
A2: P,Q,R,S are_collinear and
A3: P <> R and
A4: P <> S and
A5: Q <> R and
A6: Q <> S ; :: thesis: ( cross-ratio-tuple x = cross-ratio-tuple (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 x) )
A8: ex P9, Q9, R9, S9 being Element of V st
( P9 = x . 1 & Q9 = x . 2 & R9 = x . 3 & S9 = x . 4 & cross-ratio-tuple x = cross-ratio (P9,Q9,R9,S9) ) by Def03;
H1: ex P99, Q99, R99, S99 being Element of V st
( P99 = (pi_2143 x) . 1 & Q99 = (pi_2143 x) . 2 & R99 = (pi_2143 x) . 3 & S99 = (pi_2143 x) . 4 & cross-ratio-tuple (pi_2143 x) = cross-ratio (P99,Q99,R99,S99) ) by Def03;
ex P99, Q99, R99, S99 being Element of V st
( P99 = (pi_4321 x) . 1 & Q99 = (pi_4321 x) . 2 & R99 = (pi_4321 x) . 3 & S99 = (pi_4321 x) . 4 & cross-ratio-tuple (pi_4321 x) = cross-ratio (P99,Q99,R99,S99) ) by Def03;
hence ( cross-ratio-tuple x = cross-ratio-tuple (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 x) ) by H1, A6, A1, A8, A2, A3, A4, A5, Th34, Th34bis; :: thesis: verum