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;

( 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

hence
x = x1
by A1, ARYTM_0:def 5; :: thesis: verumassume
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;then x = (0,1) --> (x1,x2) by A1, ARYTM_0:def 5;

hence contradiction by A2, ARYTM_0:8; :: thesis: verum