let X be set ; :: thesis: for Y being complex-functions-membered set

for f being PartFunc of X,Y holds abs (abs f) = abs f

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y holds abs (abs f) = abs f

let f be PartFunc of X,Y; :: thesis: abs (abs f) = abs f

set f1 = abs f;

thus A1: dom (abs (abs f)) = dom (abs f) by Def36; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom (abs (abs f)) or (abs (abs f)) . b_{1} = (abs f) . b_{1} )

let x be object ; :: thesis: ( not x in dom (abs (abs f)) or (abs (abs f)) . x = (abs f) . x )

assume A2: x in dom (abs (abs f)) ; :: thesis: (abs (abs f)) . x = (abs f) . x

hence (abs (abs f)) . x = abs ((abs f) . x) by Def36

.= abs (abs (f . x)) by A1, A2, Def36

.= (abs f) . x by A1, A2, Def36 ;

:: thesis: verum

for f being PartFunc of X,Y holds abs (abs f) = abs f

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y holds abs (abs f) = abs f

let f be PartFunc of X,Y; :: thesis: abs (abs f) = abs f

set f1 = abs f;

thus A1: dom (abs (abs f)) = dom (abs f) by Def36; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom (abs (abs f)) or (abs (abs f)) . x = (abs f) . x )

assume A2: x in dom (abs (abs f)) ; :: thesis: (abs (abs f)) . x = (abs f) . x

hence (abs (abs f)) . x = abs ((abs f) . x) by Def36

.= abs (abs (f . x)) by A1, A2, Def36

.= (abs f) . x by A1, A2, Def36 ;

:: thesis: verum