let V be RealLinearSpace; :: thesis: for x being Tuple of 4, the carrier of V holds cross-ratio-tuple (pi_1243 x) = 1 / (cross-ratio-tuple x)
let x be Tuple of 4, the carrier of V; :: thesis: cross-ratio-tuple (pi_1243 x) = 1 / (cross-ratio-tuple x)
consider P9, Q9, R9, S9 being Element of V such that
A1: ( P9 = x . 1 & Q9 = x . 2 & R9 = x . 3 & S9 = x . 4 & cross-ratio-tuple x = cross-ratio (P9,Q9,R9,S9) ) by Def03;
ex P99, Q99, R99, S99 being Element of V st
( P99 = (pi_1243 x) . 1 & Q99 = (pi_1243 x) . 2 & R99 = (pi_1243 x) . 3 & S99 = (pi_1243 x) . 4 & cross-ratio-tuple (pi_1243 x) = cross-ratio (P99,Q99,R99,S99) ) by Def03;
hence cross-ratio-tuple (pi_1243 x) = 1 / (cross-ratio-tuple x) by A1, XCMPLX_1:57; :: thesis: verum