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 :: thesis: for x being object st x in Line ((f . a),(f . b)) holds
x in f .: (Line (a,b))

let x be object ; :: 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 Th1;
LIN f . a,f . b,f . y by A2, A3, AFF_1:def 2;
then LIN a,b,y by A1, Th88;
then y in Line (a,b) by AFF_1:def 2;
hence x in f .: (Line (a,b)) by A3, Th91; :: thesis: verum

end;

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

now :: thesis: for x being object st x in f .: (Line (a,b)) holds
x in Line ((f . a),(f . b))

let x be object ; :: 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, Th91;
LIN a,b,y by A6, AFF_1:def 2;
then LIN f . a,f . b,x9 by A1, A7, Th88;
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