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
ex r being non zero non unit Real st
( r = cross-ratio-tuple x & cross-ratio-tuple (pi_1243 x) = op1 r )
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
ex r being non zero non unit Real st
( r = cross-ratio-tuple x & cross-ratio-tuple (pi_1243 x) = op1 r )
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 ex r being non zero non unit Real st
( r = cross-ratio-tuple x & cross-ratio-tuple (pi_1243 x) = op1 r ) )
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: ex r being non zero non unit Real st
( r = cross-ratio-tuple x & cross-ratio-tuple (pi_1243 x) = op1 r )
A4: ( P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q ) by A2, ZFMISC_1:def 6;
consider P9, Q9, R9, S9 being Element of V such that
A5: ( P9 = x . 1 & Q9 = x . 2 & R9 = x . 3 & S9 = x . 4 & cross-ratio-tuple x = cross-ratio (P9,Q9,R9,S9) ) by Def03;
reconsider r = cross-ratio-tuple x as non zero non unit Real by Def01, A1, A3, A5, A4, Th32, Th31;
take r ; :: thesis: ( r = cross-ratio-tuple x & cross-ratio-tuple (pi_1243 x) = op1 r )
thus ( r = cross-ratio-tuple x & cross-ratio-tuple (pi_1243 x) = op1 r ) by Th39; :: thesis: verum