reconsider u = |[1,0,1]| as non zero Element of (TOP-REAL 3) ;
reconsider P = Dir u as Element of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
now :: thesis: ( u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) )
thus u . 3 = u `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: |[(u . 1),(u . 2)]| in circle (0,0,1)
now :: thesis: ( u . 1 = 1 & u . 2 = 0 )
thus u . 1 = u `1 by EUCLID_5:def 1
.= 1 by EUCLID_5:2 ; :: thesis: u . 2 = 0
thus u . 2 = u `2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2 ; :: thesis: verum
end;
then ( (u . 1) * (u . 1) = 1 & (u . 2) * (u . 2) = 0 ) ;
then ( (u . 1) ^2 = 1 & (u . 2) ^2 = 0 ) by SQUARE_1:def 1;
then ((u . 1) ^2) + ((u . 2) ^2) = 1 ;
hence |[(u . 1),(u . 2)]| in circle (0,0,1) by BKMODEL1:13; :: thesis: verum
end;
then P is Element of absolute by BKMODEL1:86;
hence Dir |[1,0,1]| is Element of absolute ; :: thesis: verum