let AFS be AffinSpace; :: thesis: for f being Permutation of the carrier of AFS
for K being Subset of AFS st f is collineation & K is being_line holds
f .: K is being_line
let f be Permutation of the carrier of AFS; :: thesis: for K being Subset of AFS st f is collineation & K is being_line holds
f .: K is being_line
let K be Subset of AFS; :: thesis: ( f is collineation & K is being_line implies f .: K is being_line )
assume that
A1: f is collineation and
A2: K is being_line ; :: thesis: f .: K is being_line
consider a, b being Element of AFS such that
A3: ( a <> b & K = Line a,b ) by A2, AFF_1:def 3;
set p = f . a;
set q = f . b;
A4: f .: K = Line (f . a),(f . b) by A1, A3, Th113;
f . a <> f . b by A3, FUNCT_2:85;
hence f .: K is being_line by A4, AFF_1:def 3; :: thesis: verum