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

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