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