let x, y be Element of REAL ; :: thesis: ( [*x,y*] in REAL implies y = 0 )
assume A1: [*x,y*] in REAL ; :: thesis: y = 0
assume y <> 0 ; :: thesis: contradiction
then [*x,y*] = (0,1) --> (x,y) by Def5;
hence contradiction by A1, Th8; :: thesis: verum