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 S1[ Nat] means ((power F_Real) . ((- (1_ F_Real)),$1)) * j in INT ;
P1: S1[ 0 ]
proof
((power F_Real) . ((- (1_ F_Real)),0)) * j = (1_ F_Real) * j by GROUP_1:def 7
.= j ;
hence S1[ 0 ] by AS; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AS1: S1[n] ; :: thesis: S1[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 S1[n] from NAT_1:sch 2(P1, P2);
 hence ((power F_Real) . ((- (1_ F_Real)),i)) * j in INT ; :: thesis: verum