let x be Real; :: 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 Def1;

hereby :: thesis: x = x1

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

end;

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