let i be Nat; :: thesis: for j being Element of F_Real
for k being Element of F_Rat st j = k holds
(() . ((- ()),i)) * j = (() . ((- ()),i)) * k

let j be Element of F_Real; :: thesis: for k being Element of F_Rat st j = k holds
(() . ((- ()),i)) * j = (() . ((- ()),i)) * k

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