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 Element of 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:61;
assume <*a,b*> in y=0-line ; :: thesis: ( a in REAL & b = 0 )
then consider x, y being Element of REAL such that
A3: <*a,b*> = |[x,0 ]| by A1;
<*a,b*> . 1 = x by A3, FINSEQ_1:61;
hence a in REAL by A2; :: thesis: b = 0
<*a,b*> . 2 = b by FINSEQ_1:61;
hence b = 0 by A3, FINSEQ_1:61; :: 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