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 ;
then LIN a,b,y by ;
then y in Line (a,b) by AFF_1:def 2;
hence x in f .: (Line (a,b)) by ; :: 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 ;
LIN a,b,y by ;
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 ; :: thesis: verum