let AFS be AffinSpace; :: thesis: for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is collineation holds
f .: (Line a,b) = Line (f . a),(f . b)
let a, b be Element of AFS; :: thesis: for f being Permutation of the carrier of AFS st f is collineation holds
f .: (Line a,b) = Line (f . a),(f . b)
let f be Permutation of the carrier of AFS; :: thesis: ( f is collineation implies f .: (Line a,b) = Line (f . a),(f . b) )
assume A1: f is collineation ; :: thesis: f .: (Line a,b) = Line (f . a),(f . b)

now

let x be set ; :: thesis: ( x in Line (f . a),(f . b) implies x in f .: (Line a,b) )
assume A2: x in Line (f . a),(f . b) ; :: thesis: x in f .: (Line a,b)
then reconsider x9 = x as Element of AFS ;
consider y being Element of AFS such that
A3: f . y = x9 by Th2;
LIN f . a,f . b,f . y by A2, A3, AFF_1:def 2;
then LIN a,b,y by A1, Th108;
then y in Line a,b by AFF_1:def 2;
hence x in f .: (Line a,b) by A3, Th111; :: thesis: verum

end;

then A4: Line (f . a),(f . b) c= f .: (Line a,b) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in f .: (Line a,b) implies x in Line (f . a),(f . b) )
assume A5: x in f .: (Line a,b) ; :: thesis: x in Line (f . a),(f . b)
then reconsider x9 = x as Element of AFS ;
consider y being Element of AFS such that
A6: y in Line a,b and
A7: f . y = x9 by A5, Th111;
LIN a,b,y by A6, AFF_1:def 2;
then LIN f . a,f . b,x9 by A1, A7, Th108;
hence x in Line (f . a),(f . b) by AFF_1:def 2; :: thesis: verum

end;

then f .: (Line a,b) c= Line (f . a),(f . b) by TARSKI:def 3;
hence f .: (Line a,b) = Line (f . a),(f . b) by A4, XBOOLE_0:def 10; :: thesis: verum