take Dir100 ; :: thesis: Dir100 is zero_proj3
reconsider p = |[1,0,0]| as non zero Element of (TOP-REAL 3) ;

now :: thesis: for u being non zero Element of (TOP-REAL 3) st Dir100 = Dir u holds
u . 3 = 0

let u be non zero Element of (TOP-REAL 3); :: thesis: ( Dir100 = Dir u implies u . 3 = 0 )
assume Dir100 = Dir u ; :: thesis: u . 3 = 0
then are_Prop u,p by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A1: u = a * p by ANPROJ_1:1;
thus u . 3 = a * (p . 3) by A1, RVSUM_1:44
.= a * 0
.= 0 ; :: thesis: verum

end;

hence Dir100 is zero_proj3 ; :: thesis: verum