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

proof

((power F_Real) . ((- (1_ F_Real)),0)) * j = (1_ F_Real) * j by GROUP_1:def 7
.= ((power F_Rat) . ((- (1_ F_Rat)),0)) * k by AS, GROUP_1:def 7 ;
hence S₁[ 0 ] ; :: 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) ;
((power F_Rat) . ((- (1_ F_Rat)),(n + 1))) * k = (((power F_Rat) . ((- (1_ F_Rat)),n)) * (- (1_ F_Rat))) * k by GROUP_1:def 7
.= (- (1_ F_Rat)) * (((power F_Rat) . ((- (1_ F_Rat)),n)) * k) ;
hence ((power F_Real) . ((- (1_ F_Real)),(n + 1))) * j = ((power F_Rat) . ((- (1_ F_Rat)),(n + 1))) * k by AS1, P3; :: 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 = ((power F_Rat) . ((- (1_ F_Rat)),i)) * k ; :: thesis: verum