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 and
A4: K = Line (a,b) by A2, AFF_1:def 3;
set q = f . b;
set p = f . a;
A5: f . a <> f . b by A3, FUNCT_2:58;
f .: K = Line ((f . a),(f . b)) by A1, A4, Th93;
hence f .: K is being_line by A5, AFF_1:def 3; :: thesis: verum