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 )

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