let x1, x2, x3, x4, y1, y2, y3, y4 be 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 )
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 ) ; :: thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
then A3: [*x1,x2,x3,x4*] = [*xx1,xx2*] by Lm3;
A4: now :: thesis: ( not y3 <> 0 & not y4 <> 0 )
assume ( y3 <> 0 or y4 <> 0 ) ; :: thesis: contradiction
then [*xx1,xx2*] = (0,1,2,3) --> (y1,y2,y3,y4) by A1, A3, Def5;
hence contradiction by Th4; :: thesis: 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; :: 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, Def5;
now :: thesis: ( y3 = 0 implies not y4 = 0 )
assume that
A6: y3 = 0 and
A7: y4 = 0 ; :: thesis: contradiction
[*y1,y2,y3,y4*] = [*yy1,yy2*] by A6, A7, Lm3;
hence contradiction by A5, Th4; :: thesis: 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; :: thesis: verum
end;
end;