let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS holds
( f is collineation iff for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) )
let f be Permutation of the carrier of AFS; :: thesis: ( f is collineation iff for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) )
thus ( f is collineation implies for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) ) :: thesis: ( ( for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) ) implies f is collineation )

proof

assume A1: f is_automorphism_of the CONGR of AFS ; :: according to TRANSGEO:def 12 :: thesis: for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t )
let x, y, z, t be Element of AFS; :: thesis: ( x,y // z,t iff f . x,f . y // f . z,f . t )
thus ( x,y // z,t implies f . x,f . y // f . z,f . t ) :: thesis: ( f . x,f . y // f . z,f . t implies x,y // z,t )

proof

assume x,y // z,t ; :: thesis: f . x,f . y // f . z,f . t
then [[x,y],[z,t]] in the CONGR of AFS by ANALOAF:def 2;
then [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS by A1;
hence f . x,f . y // f . z,f . t by ANALOAF:def 2; :: thesis: verum

end;

assume f . x,f . y // f . z,f . t ; :: thesis: x,y // z,t
then [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS by ANALOAF:def 2;
then [[x,y],[z,t]] in the CONGR of AFS by A1;
hence x,y // z,t by ANALOAF:def 2; :: thesis: verum

end;

assume A2: for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) ; :: thesis: f is collineation
let x be Element of AFS; :: according to TRANSGEO:def 3,TRANSGEO:def 12 :: thesis: for y, z, t being Element of the carrier of AFS holds
( [[x,y],[z,t]] in the CONGR of AFS iff [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS )
let y, z, t be Element of AFS; :: thesis: ( [[x,y],[z,t]] in the CONGR of AFS iff [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS )
( x,y // z,t iff f . x,f . y // f . z,f . t ) by A2;
hence ( [[x,y],[z,t]] in the CONGR of AFS iff [[(f . x),(f . y)],[(f . z),(f . t)]] in the CONGR of AFS ) by ANALOAF:def 2; :: thesis: verum