defpred S₁[ object , object ] means ex x being Real st
( $1 = x & $2 = [x,(- x)] );
A1: for r being object st r in REAL holds
ex a being object st
( a in real-anti-diagonal & S₁[r,a] )

let r be object ; :: thesis:
assume r in REAL ; :: thesis:
then reconsider r = r as Real ;
set a = [r,(- r)];
[r,(- r)] in real-anti-diagonal ;
hence ex a being object st
( a in real-anti-diagonal & S₁[r,a] ) ; :: thesis:

end;

reconsider x = 1, y = - 1 as Element of REAL by XREAL_0:def 1;
set z = [x,y];
[x,y] in real-anti-diagonal ;
hence real-anti-diagonal <> {} ; :: thesis:

end;

let r1, r2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A4: ( r1 in dom Z & r2 in dom Z ) and
A5: Z . r1 = Z . r2 ; :: thesis:
consider x1 being Real such that
A6: ( r1 = x1 & Z . r1 = [x1,(- x1)] ) by A2, A4;
consider x2 being Real such that
A7: ( r2 = x2 & Z . r2 = [x2,(- x2)] ) by A2, A4;
thus r1 = r2 by A6, A7, A5, XTUPLE_0:1; :: thesis:

end;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in real-anti-diagonal ; :: thesis:
then consider x, y being Real such that
A8: z = [x,y] and
A9: y = - x ;
consider x1 being Real such that
A10: ( x = x1 & Z . x = [x1,(- x1)] ) by A2, XREAL_0:def 1;
thus z in rng Z by A10, A8, A9, FUNCT_2:4, A3, XREAL_0:def 1; :: thesis:

end;