let x1, x2, x3, x4, y1, y2, y3, y4 be Element of REAL ; :: thesis: ( [*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*] ; :: thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

per cases ( ( x3 = 0 & x4 = 0 ) or x3 <> 0 or x4 <> 0 ) ;

suppose A2: ( x3 = 0 & x4 = 0 ) ; :: thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

then A3: [*x1,x2,x3,x4*] = [*x1,x2*] by Lm4;

A4: now

assume ( y3 <> 0 or y4 <> 0 ) ; :: thesis: contradiction
then [*x1,x2*] = (0,1,2,3) --> (y1,y2,y3,y4) by A1, A3, Def6;
hence contradiction by Th10; :: thesis: verum

end;

then [*y1,y2,y3,y4*] = [*y1,y2*] by Lm4;
hence ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) by A1, A2, A3, A4, ARYTM_0:12; :: thesis: verum

end;

suppose ( x3 <> 0 or x4 <> 0 ) ; :: thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )

then A5: [*y1,y2,y3,y4*] = (0,1,2,3) --> (x1,x2,x3,x4) by A1, Def6;

now

assume that
A6: y3 = 0 and
A7: y4 = 0 ; :: thesis: contradiction
[*y1,y2,y3,y4*] = [*y1,y2*] by A6, A7, Lm4;
hence contradiction by A5, Th10; :: thesis: verum

end;

then [*y1,y2,y3,y4*] = (0,1,2,3) --> (y1,y2,y3,y4) by Def6;
hence ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) by A5, Lm1, Th11; :: thesis: verum

end;

end;