now :: thesis: for x being object st x in dom (f to_power k) holds
0 <= (f to_power k) . x

let x be object ; :: thesis: ( x in dom (f to_power k) implies 0 <= (f to_power k) . b₁ )
assume A1: x in dom (f to_power k) ; :: thesis: 0 <= (f to_power k) . b₁

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: 0 <= (f to_power k) . b₁

then (f . x) to_power k = 1 by POWER:24;
hence 0 <= (f to_power k) . x by A1, Def4; :: thesis: verum

end;

suppose A2: k > 0 ; :: thesis: 0 <= (f to_power k) . b₁

per cases ( 0 < f . x or 0 = f . x ) by MESFUNC6:51;

suppose 0 < f . x ; :: thesis: 0 <= (f to_power k) . b₁

then 0 < (f . x) to_power k by POWER:34;
hence 0 <= (f to_power k) . x by A1, Def4; :: thesis: verum

end;

suppose 0 = f . x ; :: thesis: 0 <= (f to_power k) . b₁

then 0 = (f . x) to_power k by A2, POWER:def 2;
hence 0 <= (f to_power k) . x by A1, Def4; :: thesis: verum

end;

end;

end;

end;

end;

hence f to_power k is nonnegative by MESFUNC6:52; :: thesis: verum