theorem Ta2: :: ANPROJ_9:20

1_ GroupHomography3 = homography (1. (F_Real,3))