let P be Element of BK_model ; :: thesis: for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds
((u . 1) ^2) + ((u . 2) ^2) < 1
let u be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u & u . 3 = 1 implies ((u . 1) ^2) + ((u . 2) ^2) < 1 )
assume that
A1: P = Dir u and
A2: u . 3 = 1 ; :: thesis: ((u . 1) ^2) + ((u . 2) ^2) < 1
consider u2 being non zero Element of (TOP-REAL 3) such that
A3: ( Dir u2 = P & u2 . 3 = 1 & BK_to_REAL2 P = |[(u2 . 1),(u2 . 2)]| ) by Def01;
A4: u = u2 by A1, A2, A3, BKMODEL1:43;
reconsider S = |[(u . 1),(u . 2)]| as Element of (TOP-REAL 2) ;
A5: |.(S - |[0,0]|).| = |.(|[(S `1),(S `2)]| - |[0,0]|).| by EUCLID:53
.= |.|[((S `1) - 0),((S `2) - 0)]|.| by EUCLID:62
.= |.S.| by EUCLID:53 ;
1 ^2 = 1 ;
then |.S.| ^2 < 1 by A4, A3, TOPREAL9:45, A5, SQUARE_1:16;
then ((S `1) ^2) + ((S `2) ^2) < 1 by JGRAPH_3:1;
then ((u . 1) ^2) + ((S `2) ^2) < 1 by EUCLID:52;
hence ((u . 1) ^2) + ((u . 2) ^2) < 1 by EUCLID:52; :: thesis: verum