let k be positive Real; :: thesis: for X being non empty set holds (X --> 0) to_power k = X --> 0
let X be non empty set ; :: thesis: (X --> 0) to_power k = X --> 0
A1: dom ((X --> 0) to_power k) = dom (X --> 0) by MESFUN6C:def 4;
now :: thesis: for x being Element of X st x in dom ((X --> 0) to_power k) holds
((X --> 0) to_power k) . x = (X --> 0) . x
let x be Element of X; :: thesis: ( x in dom ((X --> 0) to_power k) implies ((X --> 0) to_power k) . x = (X --> 0) . x )
assume x in dom ((X --> 0) to_power k) ; :: thesis: ((X --> 0) to_power k) . x = (X --> 0) . x
then ((X --> 0) to_power k) . x = ((X --> 0) . x) to_power k by MESFUN6C:def 4;
then ((X --> 0) to_power k) . x = 0 to_power k by FUNCOP_1:7;
then ((X --> 0) to_power k) . x = 0 by POWER:def 2;
hence ((X --> 0) to_power k) . x = (X --> 0) . x by FUNCOP_1:7; :: thesis: verum
end;
hence (X --> 0) to_power k = X --> 0 by A1, PARTFUN1:5; :: thesis: verum