let AFS be AffinSpace; :: thesis: for f, g being Permutation of the carrier of AFS st f is collineation & g is collineation holds

( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )

let f, g be Permutation of the carrier of AFS; :: thesis: ( f is collineation & g is collineation implies ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation ) )

assume ( f is_automorphism_of the CONGR of AFS & g is_automorphism_of the CONGR of AFS ) ; :: according to TRANSGEO:def 12 :: thesis: ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )

hence ( f " is_automorphism_of the CONGR of AFS & f * g is_automorphism_of the CONGR of AFS ) by Th17, Th18; :: according to TRANSGEO:def 12 :: thesis: id the carrier of AFS is collineation

thus id the carrier of AFS is_automorphism_of the CONGR of AFS ; :: according to TRANSGEO:def 12 :: thesis: verum

( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )

let f, g be Permutation of the carrier of AFS; :: thesis: ( f is collineation & g is collineation implies ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation ) )

assume ( f is_automorphism_of the CONGR of AFS & g is_automorphism_of the CONGR of AFS ) ; :: according to TRANSGEO:def 12 :: thesis: ( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )

hence ( f " is_automorphism_of the CONGR of AFS & f * g is_automorphism_of the CONGR of AFS ) by Th17, Th18; :: according to TRANSGEO:def 12 :: thesis: id the carrier of AFS is collineation

thus id the carrier of AFS is_automorphism_of the CONGR of AFS ; :: according to TRANSGEO:def 12 :: thesis: verum