let a be Real; :: thesis: for x1, x2 being Element of REAL st a = [*x1,x2*] holds
( x2 = 0 & a = x1 )
let x1, x2 be Element of REAL ; :: thesis: ( a = [*x1,x2*] implies ( x2 = 0 & a = x1 ) )
assume A1: a = [*x1,x2*] ; :: thesis: ( x2 = 0 & a = x1 )
A2: a in REAL by XREAL_0:def 1;

hereby :: thesis: a = x1

assume x2 <> 0 ; :: thesis: contradiction
then a = (0,1) --> (x1,x2) by A1, ARYTM_0:def 5;
hence contradiction by A2, ARYTM_0:8; :: thesis: verum

end;

hence a = x1 by A1, ARYTM_0:def 5; :: thesis: verum