let a, b be set ; :: thesis: ( <*a,b*> in y=0-line iff ( a in REAL & b = 0 ) )
A1: ( <*a,b*> in y=0-line iff ex x being Real st <*a,b*> = |[x,0]| ) ;

hereby :: thesis: ( a in REAL & b = 0 implies <*a,b*> in y=0-line )

A2: <*a,b*> . 1 = a by FINSEQ_1:44;
assume <*a,b*> in y=0-line ; :: thesis: ( a in REAL & b = 0 )
then consider x, y being Real such that
A3: <*a,b*> = |[x,0]| by A1;
<*a,b*> . 1 = x by A3, FINSEQ_1:44;
hence a in REAL by A2, XREAL_0:def 1; :: thesis: b = 0
<*a,b*> . 2 = b by FINSEQ_1:44;
hence b = 0 by A3, FINSEQ_1:44; :: thesis: verum

end;

assume a in REAL ; :: thesis: ( not b = 0 or <*a,b*> in y=0-line )
then reconsider x = a as Real ;
|[x,0]| = <*a,0*> ;
hence ( not b = 0 or <*a,b*> in y=0-line ) ; :: thesis: verum