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₁ being object holds
( not b₁ in dom (abs (abs f)) or (abs (abs f)) . b₁ = (abs f) . 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