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