let V be RealLinearSpace; 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*> holds
cross-ratio (P,Q,R,S) = cross-ratio-tuple x
let P, Q, R, S be Element of V; for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> holds
cross-ratio (P,Q,R,S) = cross-ratio-tuple x
let x be Tuple of 4, the carrier of V; ( x = <*P,Q,R,S*> implies cross-ratio (P,Q,R,S) = cross-ratio-tuple x )
assume
x = <*P,Q,R,S*>
; cross-ratio (P,Q,R,S) = cross-ratio-tuple x
then
( x . 1 = P & x . 2 = Q & x . 3 = R & x . 4 = S )
;
hence
cross-ratio (P,Q,R,S) = cross-ratio-tuple x
by Def03; verum