defpred S_{1}[ 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_{1}[z,c] )
and

A2: for z being Element of X st z in dom F holds

S_{1}[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 ) )

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

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

A2: for z being Element of X st z in dom F holds

S

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 ) )

hence
dom F = dom f
by SUBSET_1:3; :: thesis: for x being Element of X st x in dom F 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 ) )

end;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;assume z in dom f ; :: thesis: z in dom F

hence z in dom F by A1, A3; :: thesis: verum

hereby :: thesis: verum

assume
z in dom F
; :: thesis: z in dom f

then ex c being Element of REAL st S_{1}[z,c]
by A1;

hence z in dom f ; :: thesis: verum

end;then ex c being Element of REAL st S

hence z in dom f ; :: thesis: verum

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