let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds
( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )
let f be PartFunc of X,REAL; :: thesis: ( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )
dom (- f) = dom f by VALUED_1:8;
then dom ((- f) to_power 2) = dom f by MESFUN6C:def 4;
then A1: dom (f to_power 2) = dom ((- f) to_power 2) by MESFUN6C:def 4;
dom (abs f) = dom f by VALUED_1:def 11;
then A2: dom ((abs f) to_power 2) = dom f by MESFUN6C:def 4;
then A3: dom (f to_power 2) = dom ((abs f) to_power 2) by MESFUN6C:def 4;
for x being Element of X st x in dom (f to_power 2) holds
( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x )
proof
let x be Element of X; :: thesis: ( x in dom (f to_power 2) implies ( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x ) )
assume A4: x in dom (f to_power 2) ; :: thesis: ( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x )
then A5: ( x in dom ((- f) to_power 2) & x in dom (f to_power 2) & x in dom f & x in dom (- f) & x in dom ((abs f) to_power 2) ) by A2, A1, MESFUN6C:def 4;
A6: ((- f) to_power 2) . x = ((- f) . x) to_power 2 by A4, A1, MESFUN6C:def 4
.= (- (f . x)) to_power 2 by VALUED_1:8
.= (f . x) to_power 2 by FIB_NUM3:3
.= (f to_power 2) . x by A4, MESFUN6C:def 4 ;
((abs f) to_power 2) . x = (f to_power 2) . x
proof
A7: ((abs f) to_power 2) . x = ((abs f) . x) to_power 2 by A5, MESFUN6C:def 4
.= |.(f . x).| to_power 2 by VALUED_1:18 ;
now :: thesis: ( ( ((abs f) to_power 2) . x = (f . x) to_power 2 & ((abs f) to_power 2) . x = (f to_power 2) . x ) or ( ((abs f) to_power 2) . x = (- (f . x)) to_power 2 & ((abs f) to_power 2) . x = (f to_power 2) . x ) )
per cases ( ((abs f) to_power 2) . x = (f . x) to_power 2 or ((abs f) to_power 2) . x = (- (f . x)) to_power 2 ) by A7, ABSVALUE:1;
case ((abs f) to_power 2) . x = (f . x) to_power 2 ; :: thesis: ((abs f) to_power 2) . x = (f to_power 2) . x
hence ((abs f) to_power 2) . x = (f to_power 2) . x by A4, MESFUN6C:def 4; :: thesis: verum
end;
case ((abs f) to_power 2) . x = (- (f . x)) to_power 2 ; :: thesis: ((abs f) to_power 2) . x = (f to_power 2) . x
then ((abs f) to_power 2) . x = (f . x) to_power 2 by FIB_NUM3:3
.= (f to_power 2) . x by A4, MESFUN6C:def 4 ;
hence ((abs f) to_power 2) . x = (f to_power 2) . x ; :: thesis: verum
end;
end;
end;
hence ((abs f) to_power 2) . x = (f to_power 2) . x ; :: thesis: verum
end;
hence ( (f to_power 2) . x = ((- f) to_power 2) . x & (f to_power 2) . x = ((abs f) to_power 2) . x ) by A6; :: thesis: verum
end;
then ( ( for x being Element of X st x in dom (f to_power 2) holds
(f to_power 2) . x = ((- f) to_power 2) . x ) & ( for x being Element of X st x in dom (f to_power 2) holds
(f to_power 2) . x = ((abs f) to_power 2) . x ) ) ;
hence ( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 ) by A1, A3, PARTFUN1:5; :: thesis: verum