let x1, x2, x3, x4, y1, y2, y3, y4 be Real; ( [*x1,x2,x3,x4*] = [*y1,y2,y3,y4*] implies ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) )
assume A1:
[*x1,x2,x3,x4*] = [*y1,y2,y3,y4*]
; ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
reconsider xx1 = x1, xx2 = x2, yy1 = y1, yy2 = y2 as Element of REAL by XREAL_0:def 1;
per cases
( ( x3 = 0 & x4 = 0 ) or x3 <> 0 or x4 <> 0 )
;
suppose A2:
(
x3 = 0 &
x4 = 0 )
;
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )then A3:
[*x1,x2,x3,x4*] = [*xx1,xx2*]
by Lm3;
A4:
now ( not y3 <> 0 & not y4 <> 0 )assume
(
y3 <> 0 or
y4 <> 0 )
;
contradictionthen
[*xx1,xx2*] = (
0,1,2,3)
--> (
y1,
y2,
y3,
y4)
by A1, A3, Def5;
hence
contradiction
by Th4;
verum end; then
[*y1,y2,y3,y4*] = [*yy1,yy2*]
by Lm3;
hence
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 )
by A1, A2, A3, A4, ARYTM_0:10;
verum end; suppose
(
x3 <> 0 or
x4 <> 0 )
;
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )then A5:
[*y1,y2,y3,y4*] = (
0,1,2,3)
--> (
x1,
x2,
x3,
x4)
by A1, Def5;
now ( y3 = 0 implies not y4 = 0 )assume that A6:
y3 = 0
and A7:
y4 = 0
;
contradiction
[*y1,y2,y3,y4*] = [*yy1,yy2*]
by A6, A7, Lm3;
hence
contradiction
by A5, Th4;
verum end; then
[*y1,y2,y3,y4*] = (
0,1,2,3)
--> (
y1,
y2,
y3,
y4)
by Def5;
hence
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 )
by A5, Lm1, FUNCT_4:146;
verum end; end;