theorem Th55: :: ANPROJ_8:67
( Col ((1. (F_Real,3)),1) = <*1,0,0*> & Col ((1. (F_Real,3)),2) = <*0,1,0*> & Col ((1. (F_Real,3)),3) = <*0,0,1*> )