defpred S1[ 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 S1[z,c] ) and
A2: for z being Element of X st z in dom F holds
S1[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 ) end;
hereby :: thesis: verum
assume z in dom F ; :: thesis: z in dom f
then ex c being Element of REAL st S1[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