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 6;
then LDOM3: dom (f to_power 2) = dom ((- f) to_power 2) by MESFUN6C:def 6;
dom (abs f) = dom f by VALUED_1:def 11;
then LDOM6: dom ((abs f) to_power 2) = dom f by MESFUN6C:def 6;
then LDOM6P: dom (f to_power 2) = dom ((abs f) to_power 2) by MESFUN6C:def 6;
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 LDOMP: 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 LDOM: ( 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 LDOM6, MESFUN6C:def 6, LDOM3;
C1: ((- f) to_power 2) . x = ((- f) . x) to_power 2 by MESFUN6C:def 6, LDOMP, LDOM3
.= (- (f . x)) to_power 2 by VALUED_1:8
.= (f . x) to_power 2 by FIB_NUM3:3
.= (f to_power 2) . x by MESFUN6C:def 6, LDOMP ;
((abs f) to_power 2) . x = (f to_power 2) . x

proof

LABP: ((abs f) to_power 2) . x = ((abs f) . x) to_power 2 by MESFUN6C:def 6, LDOM
.= (abs (f . x)) to_power 2 by VALUED_1:18 ;

now

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 LABP, 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 MESFUN6C:def 6, LDOMP; :: 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 MESFUN6C:def 6, LDOMP ;
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 C1; :: 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 PARTFUN1:34, LDOM3, LDOM6P; :: thesis: verum