let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ex a, b, c being Element of F_Real st
( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )
consider u being Element of (TOP-REAL 3) such that
A1: not u is zero and
A2: P = Dir u by ANPROJ_1:26;
A3: u = |[(u `1),(u `2),(u `3)]| by EUCLID_5:3
.= |[(u . 1),(u `2),(u `3)]| by EUCLID_5:def 1
.= |[(u . 1),(u . 2),(u `3)]| by EUCLID_5:def 2
.= |[(u . 1),(u . 2),(u . 3)]| by EUCLID_5:def 3 ;
reconsider a = u . 1, b = u . 2, c = u . 3 as Element of F_Real by XREAL_0:def 1;
take a ; :: thesis: ex b, c being Element of F_Real st
( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )
take b ; :: thesis: ex c being Element of F_Real st
( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )
take c ; :: thesis: ( P = Dir |[a,b,c]| & ( a <> 0 or b <> 0 or c <> 0 ) )
thus P = Dir |[a,b,c]| by A2, A3; :: thesis: ( a <> 0 or b <> 0 or c <> 0 )
thus ( a <> 0 or b <> 0 or c <> 0 ) by A1, A3, EUCLID_5:4; :: thesis: verum