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

( 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