deffunc H₁( set ) -> R_eal = (f . $1) |^ k;
defpred S₁[ set ] means $1 in dom f;
consider f3 being PartFunc of X,ExtREAL such that
A1: for d being Element of X holds
( d in dom f3 iff S₁[d] ) and
A2: for d being Element of X st d in dom f3 holds
f3 /. d = H₁(d) from PARTFUN2:sch 2();
take f3 ; :: thesis: ( dom f3 = dom f & ( for x being Element of X st x in dom f3 holds
f3 . x = (f . x) |^ k ) )
for x being object st x in dom f holds
x in dom f3 by A1;
then A3: dom f c= dom f3 ;
for x being object st x in dom f3 holds
x in dom f by A1;
then dom f3 c= dom f ;
hence dom f3 = dom f by A3, XBOOLE_0:def 10; :: thesis: for x being Element of X st x in dom f3 holds
f3 . x = (f . x) |^ k
let d be Element of X; :: thesis: ( d in dom f3 implies f3 . d = (f . d) |^ k )
assume A4: d in dom f3 ; :: thesis: f3 . d = (f . d) |^ k
then f3 /. d = (f . d) |^ k by A2;
hence f3 . d = (f . d) |^ k by A4, PARTFUN1:def 6; :: thesis: verum