defpred S₁[ Nat] means - (uInt . $1) = uInt . (- $1);
uInt . 0 = 0_No by Def1;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
uInt . (n + 1) = [{(uInt . n)},{}] by Def1;
then ( L_ (uInt . (n + 1)) = {(uInt . n)} & R_ (uInt . (n + 1)) = {} ) ;
then - (uInt . (n + 1)) = [{},(-- {(uInt . n)})] by SURREALR:22, SURREALR:7
.= [{},{(uInt . (- n))}] by A3, SURREALR:21
.= uInt . (- (n + 1)) by Def1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A4: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let i be Integer; :: thesis: - (uInt . i) = uInt . (- i)
i in INT by INT_1:def 2;
then consider o being Nat such that
A5: ( i = o or i = - o ) by INT_1:def 1;
S₁[o] by A4;
hence - (uInt . i) = uInt . (- i) by A5; :: thesis: verum