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))

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

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))

then A4:
Line ((f . a),(f . b)) c= f .: (Line (a,b))
by TARSKI:def 3;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;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

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

x in Line ((f . a),(f . b))

then
f .: (Line (a,b)) c= Line ((f . a),(f . b))
by TARSKI:def 3;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;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

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