defpred S₁[ set , set ] means ( $1 in dom f & $2 = (f . $1) to_power k );
consider F being PartFunc of X,REAL such that
A1: for z being Element of X holds
( z in dom F iff ex c being Element of REAL st S₁[z,c] ) and
A2: for z being Element of X st z in dom F holds
S₁[z,F . z] from SEQ_1:sch 2();
take F ; :: thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds
F . x = (f . x) to_power k ) )

now :: thesis: for z being Element of X holds
( ( z in dom f implies z in dom F ) & ( z in dom F implies z in dom f ) )

let z be Element of X; :: thesis: ( ( z in dom f implies z in dom F ) & ( z in dom F implies z in dom f ) )

hereby :: thesis: ( z in dom F implies z in dom f )

A3: (f . z) to_power k is Element of REAL by XREAL_0:def 1;
assume z in dom f ; :: thesis: z in dom F
hence z in dom F by A1, A3; :: thesis: verum

end;

hereby :: thesis: verum

assume z in dom F ; :: thesis: z in dom f
then ex c being Element of REAL st S₁[z,c] by A1;
hence z in dom f ; :: thesis: verum

end;

end;

hence dom F = dom f by SUBSET_1:3; :: thesis: for x being Element of X st x in dom F holds
F . x = (f . x) to_power k
thus for x being Element of X st x in dom F holds
F . x = (f . x) to_power k by A2; :: thesis: verum