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

hereby :: thesis: x = x1

assume x2 <> 0 ; :: thesis: contradiction
then x = 0 ,1 --> x1,x2 by A1, ARYTM_0:def 7;
hence contradiction by A2, ARYTM_0:10; :: thesis: verum

end;

hence x = x1 by A1, ARYTM_0:def 7; :: thesis: verum