let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS

for A, C being Subset of AFS st f is collineation & A // C holds

f .: A // f .: C

let f be Permutation of the carrier of AFS; :: thesis: for A, C being Subset of AFS st f is collineation & A // C holds

f .: A // f .: C

let A, C be Subset of AFS; :: thesis: ( f is collineation & A // C implies f .: A // f .: C )

assume that

A1: f is collineation and

A2: A // C ; :: thesis: f .: A // f .: C

consider a, b, c, d being Element of AFS such that

A3: ( a <> b & c <> d ) and

A4: a,b // c,d and

A5: ( A = Line (a,b) & C = Line (c,d) ) by A2, AFF_1:37;

A6: f . a,f . b // f . c,f . d by A1, A4, Th87;

A7: ( f . a <> f . b & f . c <> f . d ) by A3, FUNCT_2:58;

( f .: A = Line ((f . a),(f . b)) & f .: C = Line ((f . c),(f . d)) ) by A1, A5, Th93;

hence f .: A // f .: C by A7, A6, AFF_1:37; :: thesis: verum

for A, C being Subset of AFS st f is collineation & A // C holds

f .: A // f .: C

let f be Permutation of the carrier of AFS; :: thesis: for A, C being Subset of AFS st f is collineation & A // C holds

f .: A // f .: C

let A, C be Subset of AFS; :: thesis: ( f is collineation & A // C implies f .: A // f .: C )

assume that

A1: f is collineation and

A2: A // C ; :: thesis: f .: A // f .: C

consider a, b, c, d being Element of AFS such that

A3: ( a <> b & c <> d ) and

A4: a,b // c,d and

A5: ( A = Line (a,b) & C = Line (c,d) ) by A2, AFF_1:37;

A6: f . a,f . b // f . c,f . d by A1, A4, Th87;

A7: ( f . a <> f . b & f . c <> f . d ) by A3, FUNCT_2:58;

( f .: A = Line ((f . a),(f . b)) & f .: C = Line ((f . c),(f . d)) ) by A1, A5, Th93;

hence f .: A // f .: C by A7, A6, AFF_1:37; :: thesis: verum