theorem Th34: :: BKMODEL2:45
( homography (1. (F_Real,3)) = 1_ GroupHomography3 & homography (1. (F_Real,3)) = 1_ SubGroupK-isometry )