let i be Nat; :: thesis: for j being Element of F_Real st j in INT holds
((power F_Real) . ((- (1_ F_Real)),i)) * j in INT
let j be Element of F_Real; :: thesis: ( j in INT implies ((power F_Real) . ((- (1_ F_Real)),i)) * j in INT )
assume AS: j in INT ; :: thesis: ((power F_Real) . ((- (1_ F_Real)),i)) * j in INT
defpred S₁[ Nat] means ((power F_Real) . ((- (1_ F_Real)),$1)) * j in INT ;
P1: S₁[ 0 ]

proof

((power F_Real) . ((- (1_ F_Real)),0)) * j = (1_ F_Real) * j by GROUP_1:def 7
.= j ;
hence S₁[ 0 ] by AS; :: thesis: verum

end;

P2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume AS1: S₁[n] ; :: thesis: S₁[n + 1]
P3: ((power F_Real) . ((- (1_ F_Real)),(n + 1))) * j = (((power F_Real) . ((- (1_ F_Real)),n)) * (- (1_ F_Real))) * j by GROUP_1:def 7
.= (- (1_ F_Real)) * (((power F_Real) . ((- (1_ F_Real)),n)) * j) ;
reconsider mi = - (1_ F_Real) as Integer ;
reconsider m0 = ((power F_Real) . ((- (1_ F_Real)),n)) * j as Integer by AS1;
((power F_Real) . ((- (1_ F_Real)),(n + 1))) * j = - m0 by P3;
hence ((power F_Real) . ((- (1_ F_Real)),(n + 1))) * j in INT by INT_1:def 2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(P1, P2);
hence ((power F_Real) . ((- (1_ F_Real)),i)) * j in INT ; :: thesis: verum