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*> holds
cross-ratio (P,Q,R,S) = 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*> holds
cross-ratio (P,Q,R,S) = cross-ratio-tuple x
let x be Tuple of 4, the carrier of V; :: thesis: ( x = <*P,Q,R,S*> implies cross-ratio (P,Q,R,S) = cross-ratio-tuple x )
assume x = <*P,Q,R,S*> ; :: thesis: 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; :: thesis: verum